1 #include "polarityassignment.h"
4 void computePolarities(CSolver *This) {
5 SetIteratorBooleanEdge *iterator = This->getConstraints();
6 while (iterator->hasNext()) {
7 BooleanEdge boolean = iterator->next();
8 Boolean *b = boolean.getBoolean();
9 bool isNegated = boolean.isNegated();
10 computePolarity(b, isNegated ? P_FALSE : P_TRUE);
15 void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
16 Boolean *bdst = dst.getBoolean();
17 Boolean *bsrc = src.getBoolean();
18 bool isNegated = dst.isNegated() ^ src.isNegated();
19 Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
20 updatePolarity(bdst, p);
23 void updateEdgePolarity(BooleanEdge dst, Polarity p) {
24 Boolean *bdst = dst.getBoolean();
25 bool isNegated = dst.isNegated();
28 updatePolarity(bdst, p);
31 bool updatePolarity(Boolean *This, Polarity polarity) {
32 Polarity oldpolarity = This->polarity;
33 Polarity newpolarity = (Polarity) (This->polarity | polarity);
34 This->polarity = newpolarity;
35 return newpolarity != oldpolarity;
38 void updateMustValue(Boolean *This, BooleanValue value) {
39 This->boolVal = (BooleanValue) (This->boolVal | value);
42 void computePolarity(Boolean *This, Polarity polarity) {
43 if (updatePolarity(This, polarity)) {
49 return computePredicatePolarity((BooleanPredicate *)This);
51 return computeLogicOpPolarity((BooleanLogic *)This);
58 void computePredicatePolarity(BooleanPredicate *This) {
59 if (This->undefStatus) {
60 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
62 for(uint i=0; i < This->inputs.getSize(); i++) {
63 Element * e = This->inputs.get(i);
68 void computeElement(Element *e) {
69 if (e->type == ELEMFUNCRETURN) {
70 ElementFunction *ef = (ElementFunction *) e;
72 if (ef->overflowstatus) {
73 computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
76 for(uint i=0; i < ef->inputs.getSize(); i++) {
77 Element * echild = ef->inputs.get(i);
78 computeElement(echild);
83 void computeLogicOpPolarity(BooleanLogic *This) {
84 Polarity child = computeLogicOpPolarityChildren(This);
85 uint size = This->inputs.getSize();
86 for (uint i = 0; i < size; i++) {
87 BooleanEdge b = This->inputs.get(i);
88 computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
92 BooleanValue negateBooleanValue(BooleanValue This) {
98 return BV_MUSTBEFALSE;
100 return BV_MUSTBETRUE;
106 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
109 return This->polarity;
112 return P_BOTHTRUEFALSE;
119 Polarity negatePolarity(Polarity This) {
122 case P_BOTHTRUEFALSE: