4 #include "polarityassignment.h"
7 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
8 if (constraints.contains(bexpr.negate())) {
9 constraints.remove(bexpr.negate());
12 if (constraints.contains(bexpr)) {
13 constraints.remove(bexpr);
16 replaceBooleanWithTrueNoRemove(bexpr);
19 void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
20 replaceBooleanWithTrueNoRemove(bexpr.negate());
23 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
24 updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
26 ASSERT((bexpr->boolVal != BV_UNSAT) || unsat);
28 uint size = bexpr->parents.getSize();
29 for (uint i = 0; i < size; i++) {
30 ASTNode *parent = bexpr->parents.get(i);
31 if (parent->type == ELEMFUNCRETURN) {
32 ElementFunction *ef = (ElementFunction *) parent;
33 handleFunction(ef, bexpr);
35 ASSERT(parent->type == LOGICOP);
36 BooleanLogic *logicop = (BooleanLogic *) parent;
37 switch (logicop->op) {
39 handleANDTrue(logicop, bexpr);
42 handleIFFTrue(logicop, bexpr);
54 void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
55 BooleanEdge childNegate = child.negate();
57 if (ef->overflowstatus == child) {
58 ef->overflowstatus = boolTrue;
59 } else if (ef->overflowstatus == childNegate) {
60 ef->overflowstatus = boolFalse;
65 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
67 if (oldb.isNegated()) {
72 if (constraints.contains(oldb)) {
73 constraints.remove(oldb);
74 constraints.add(newb);
75 if (newb->type == BOOLEANVAR)
76 replaceBooleanWithTrue(newb);
78 replaceBooleanWithTrueNoRemove(newb);
81 if (constraints.contains(oldb.negate())) {
82 constraints.remove(oldb.negate());
83 constraints.add(newb.negate());
84 if (newb->type == BOOLEANVAR)
85 replaceBooleanWithTrue(newb.negate());
87 replaceBooleanWithTrueNoRemove(newb.negate());
91 BooleanEdge oldbnegated = oldb.negate();
92 uint size = oldb->parents.getSize();
93 for (uint i = 0; i < size; i++) {
94 ASTNode *parent = oldb->parents.get(i);
95 if (parent->type == ELEMFUNCRETURN) {
96 ElementFunction *ef = (ElementFunction *) parent;
98 if (ef->overflowstatus == oldb) {
99 ef->overflowstatus = newb;
100 newb->parents.push(ef);
101 } else if (ef->overflowstatus == oldbnegated) {
102 ef->overflowstatus = newb.negate();
103 newb->parents.push(ef);
107 BooleanLogic *logicop = (BooleanLogic *) parent;
108 boolMap.remove(logicop); //could change parent's hash
110 uint parentsize = logicop->inputs.getSize();
111 for (uint j = 0; j < parentsize; j++) {
112 BooleanEdge b = logicop->inputs.get(j);
114 logicop->inputs.set(j, newb);
115 newb->parents.push(logicop);
116 } else if (b == oldbnegated) {
117 logicop->inputs.set(j, newb.negate());
118 newb->parents.push(logicop);
121 boolMap.put(logicop, logicop);
126 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
127 uint size = bexpr->inputs.getSize();
128 BooleanEdge b0 = bexpr->inputs.get(0);
129 BooleanEdge b1 = bexpr->inputs.get(1);
130 BooleanEdge childnegate = child.negate();
131 bexpr->replaced = true;
133 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
134 } else if (b0 == childnegate) {
135 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
136 } else if (b1 == child) {
137 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
138 } else if (b1 == childnegate) {
139 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
144 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
145 BooleanEdge childNegate = child.negate();
147 boolMap.remove(bexpr);
149 for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
150 BooleanEdge b = bexpr->inputs.get(i);
153 bexpr->inputs.remove(i);
155 } else if (b == childNegate) {
156 replaceBooleanWithFalse(bexpr);
161 uint size = bexpr->inputs.getSize();
163 bexpr->replaced = true;
164 replaceBooleanWithTrue(bexpr);
165 } else if (size == 1) {
166 bexpr->replaced = true;
167 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
169 //Won't build any of these in future cases...
170 boolMap.put(bexpr, bexpr);
174 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
175 replaceBooleanWithTrue(bexpr.negate());
178 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
179 bool isNegated = bexpr.isNegated();
180 BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
182 if (b->op == SATC_IFF) {
183 if (isTrue(b->inputs.get(0))) {
184 result = b->inputs.get(1);
185 } else if (isFalse(b->inputs.get(0))) {
186 result = b->inputs.get(1).negate();
187 } else if (isTrue(b->inputs.get(1))) {
188 result = b->inputs.get(0);
189 } else if (isFalse(b->inputs.get(1))) {
190 result = b->inputs.get(0).negate();
192 } else if (b->op == SATC_AND) {
193 uint size = b->inputs.getSize();
197 result = b->inputs.get(0);
200 return isNegated ? result.negate() : result;