1 #include "polarityassignment.h"
4 void computePolarities(CSolver *This) {
8 SetIteratorBooleanEdge *iterator = This->getConstraints();
9 while (iterator->hasNext()) {
10 BooleanEdge boolean = iterator->next();
11 Boolean *b = boolean.getBoolean();
12 bool isNegated = boolean.isNegated();
13 computePolarity(b, isNegated ? P_FALSE : P_TRUE);
18 void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
19 Boolean *bdst = dst.getBoolean();
20 Boolean *bsrc = src.getBoolean();
21 bool isNegated = dst.isNegated() ^ src.isNegated();
22 Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
23 updatePolarity(bdst, p);
26 void updateEdgePolarity(BooleanEdge dst, Polarity p) {
27 Boolean *bdst = dst.getBoolean();
28 bool isNegated = dst.isNegated();
30 p = negatePolarity(p);
31 updatePolarity(bdst, p);
34 bool updatePolarity(Boolean *This, Polarity polarity) {
35 Polarity oldpolarity = This->polarity;
36 Polarity newpolarity = (Polarity) (This->polarity | polarity);
37 This->polarity = newpolarity;
38 return newpolarity != oldpolarity;
41 void updateMustValue(Boolean *This, BooleanValue value) {
42 This->boolVal = (BooleanValue) (This->boolVal | value);
45 void computePolarity(Boolean *This, Polarity polarity) {
46 if (updatePolarity(This, polarity)) {
53 return computePredicatePolarity((BooleanPredicate *)This);
55 return computeLogicOpPolarity((BooleanLogic *)This);
62 void computePredicatePolarity(BooleanPredicate *This) {
63 if (This->undefStatus) {
64 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
66 for (uint i = 0; i < This->inputs.getSize(); i++) {
67 Element *e = This->inputs.get(i);
72 void computeElement(Element *e) {
73 if (e->type == ELEMFUNCRETURN) {
74 ElementFunction *ef = (ElementFunction *) e;
76 if (ef->overflowstatus) {
77 computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
80 for (uint i = 0; i < ef->inputs.getSize(); i++) {
81 Element *echild = ef->inputs.get(i);
82 computeElement(echild);
87 void computeLogicOpPolarity(BooleanLogic *This) {
88 Polarity child = computeLogicOpPolarityChildren(This);
89 uint size = This->inputs.getSize();
90 for (uint i = 0; i < size; i++) {
91 BooleanEdge b = This->inputs.get(i);
92 computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
96 BooleanValue negateBooleanValue(BooleanValue This) {
102 return BV_MUSTBEFALSE;
104 return BV_MUSTBETRUE;
110 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
113 return This->polarity;
116 return P_BOTHTRUEFALSE;
123 Polarity negatePolarity(Polarity This) {
126 case P_BOTHTRUEFALSE: