4 #include "polarityassignment.h"
6 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
7 if (constraints.contains(bexpr.negate())) {
8 constraints.remove(bexpr.negate());
11 if (constraints.contains(bexpr)) {
12 constraints.remove(bexpr);
15 replaceBooleanWithTrueNoRemove(bexpr);
18 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
19 updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
21 ASSERT(bexpr->boolVal != BV_UNSAT);
23 uint size = bexpr->parents.getSize();
24 for (uint i = 0; i < size; i++) {
25 Boolean *parent = bexpr->parents.get(i);
26 ASSERT(parent->type == LOGICOP);
27 BooleanLogic *logicop = (BooleanLogic *) parent;
28 switch (logicop->op) {
30 handleANDTrue(logicop, bexpr);
33 handleIFFTrue(logicop, bexpr);
44 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
46 if (oldb.isNegated()) {
51 if (constraints.contains(oldb)) {
52 constraints.remove(oldb);
53 constraints.add(newb);
54 if (newb->type == BOOLEANVAR)
55 replaceBooleanWithTrue(newb);
57 replaceBooleanWithTrueNoRemove(newb);
60 if (constraints.contains(oldb.negate())) {
61 constraints.remove(oldb.negate());
62 constraints.add(newb.negate());
63 if (newb->type == BOOLEANVAR)
64 replaceBooleanWithTrue(newb.negate());
66 replaceBooleanWithTrueNoRemove(newb.negate());
70 BooleanEdge oldbnegated = oldb.negate();
71 uint size = oldb->parents.getSize();
72 for (uint i = 0; i < size; i++) {
73 Boolean *parent = oldb->parents.get(i);
74 BooleanLogic *logicop = (BooleanLogic *) parent;
75 boolMap.remove(parent); //could change parent's hash
77 uint parentsize = logicop->inputs.getSize();
78 for (uint j = 0; j < parentsize; j++) {
79 BooleanEdge b = logicop->inputs.get(j);
81 logicop->inputs.set(j, newb);
82 newb->parents.push(parent);
83 } else if (b == oldbnegated) {
84 logicop->inputs.set(j, newb.negate());
85 newb->parents.push(parent);
88 boolMap.put(parent, parent);
92 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
93 uint size = bexpr->inputs.getSize();
94 BooleanEdge b0 = bexpr->inputs.get(0);
95 BooleanEdge b1 = bexpr->inputs.get(1);
96 BooleanEdge childnegate = child.negate();
97 bexpr->replaced = true;
99 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
100 } else if (b0 == childnegate) {
101 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
102 } else if (b1 == child) {
103 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
104 } else if (b1 == childnegate) {
105 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
110 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
111 BooleanEdge childNegate=child.negate();
113 boolMap.remove(bexpr);
115 for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
116 BooleanEdge b = bexpr->inputs.get(i);
119 bexpr->inputs.remove(i);
121 } else if (b == childNegate) {
122 replaceBooleanWithFalse(bexpr);
127 uint size=bexpr->inputs.getSize();
129 bexpr->replaced = true;
130 replaceBooleanWithTrue(bexpr);
131 } else if (size == 1) {
132 bexpr->replaced = true;
133 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
135 //Won't build any of these in future cases...
136 boolMap.put(bexpr, bexpr);
140 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
141 replaceBooleanWithTrue(bexpr.negate());
144 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
145 bool isNegated=bexpr.isNegated();
146 BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
148 if (b->op == SATC_IFF) {
149 if (isTrue(b->inputs.get(0))) {
150 result = b->inputs.get(1);
151 } else if (isFalse(b->inputs.get(0))) {
152 result = b->inputs.get(1).negate();
153 } else if (isTrue(b->inputs.get(1))) {
154 result = b->inputs.get(0);
155 } else if (isFalse(b->inputs.get(1))) {
156 result = b->inputs.get(0).negate();
158 } else if (b->op==SATC_AND) {
159 uint size = b->inputs.getSize();
163 result = b->inputs.get(0);
166 return isNegated ? result.negate() : result;