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 uint size = bexpr->parents.getSize();
22 for (uint i = 0; i < size; i++) {
23 Boolean *parent = bexpr->parents.get(i);
24 ASSERT(parent->type == LOGICOP);
25 BooleanLogic *logicop = (BooleanLogic *) parent;
26 switch (logicop->op) {
28 handleANDTrue(logicop, bexpr);
31 handleIFFTrue(logicop, bexpr);
42 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
44 if (oldb.isNegated()) {
48 if (constraints.contains(oldb)) {
49 constraints.remove(oldb);
50 constraints.add(newb);
52 if (constraints.contains(oldb.negate())) {
53 constraints.remove(oldb.negate());
54 constraints.add(newb.negate());
57 BooleanEdge oldbnegated = oldb.negate();
58 uint size = oldb->parents.getSize();
59 for (uint i = 0; i < size; i++) {
60 Boolean *parent = oldb->parents.get(i);
61 BooleanLogic *logicop = (BooleanLogic *) parent;
62 boolMap.remove(parent); //could change parent's hash
64 uint parentsize = logicop->inputs.getSize();
65 for (uint j = 0; j < parentsize; j++) {
66 BooleanEdge b = logicop->inputs.get(j);
68 logicop->inputs.set(j, newb);
69 newb->parents.push(parent);
70 } else if (b == oldbnegated) {
71 logicop->inputs.set(j, newb.negate());
72 newb->parents.push(parent);
75 boolMap.put(parent, parent);
79 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
80 uint size = bexpr->inputs.getSize();
81 BooleanEdge b0 = bexpr->inputs.get(0);
82 BooleanEdge b1 = bexpr->inputs.get(1);
83 BooleanEdge childnegate = child.negate();
84 bexpr->replaced = true;
86 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
87 } else if (b0 == childnegate) {
88 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
89 } else if (b1 == child) {
90 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
91 } else if (b1 == childnegate) {
92 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
97 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
98 BooleanEdge childNegate=child.negate();
100 boolMap.remove(bexpr);
102 for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
103 BooleanEdge b = bexpr->inputs.get(i);
106 bexpr->inputs.remove(i);
108 } else if (b == childNegate) {
109 replaceBooleanWithFalse(bexpr);
114 uint size=bexpr->inputs.getSize();
116 bexpr->replaced = true;
117 replaceBooleanWithTrue(bexpr);
118 } else if (size == 1) {
119 bexpr->replaced = true;
120 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
122 //Won't build any of these in future cases...
123 boolMap.put(bexpr, bexpr);
127 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
128 replaceBooleanWithTrue(bexpr.negate());
131 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
132 bool isNegated=bexpr.isNegated();
133 BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
135 if (b->op == SATC_IFF) {
136 if (isTrue(b->inputs.get(0))) {
137 result = b->inputs.get(1);
138 } else if (isFalse(b->inputs.get(0))) {
139 result = b->inputs.get(1).negate();
140 } else if (isTrue(b->inputs.get(1))) {
141 result = b->inputs.get(0);
142 } else if (isFalse(b->inputs.get(1))) {
143 result = b->inputs.get(0).negate();
145 } else if (b->op==SATC_AND) {
146 uint size = b->inputs.getSize();
150 result = b->inputs.get(0);
153 return isNegated ? result.negate() : result;