#include "rewriter.h"
#include "boolean.h"
#include "csolver.h"
+#include "polarityassignment.h"
+#include "element.h"
-void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
+void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
+ if (constraints.contains(bexpr.negate())) {
+ constraints.remove(bexpr.negate());
+ setUnSAT();
+ }
if (constraints.contains(bexpr)) {
constraints.remove(bexpr);
}
- uint size = bexpr->parents.getSize();
- for (uint i = 0; i < size; i++) {
- Boolean *parent = bexpr->parents.get(i);
- BooleanLogic *logicop = (BooleanLogic *) parent;
- switch (logicop->op) {
- case SATC_AND:
- handleANDTrue(logicop, bexpr);
- break;
- case SATC_OR:
- replaceBooleanWithTrue(parent);
- break;
- case SATC_NOT:
- replaceBooleanWithFalse(parent);
- break;
- case SATC_IFF:
- handleXORFalse(logicop, bexpr);
- break;
- case SATC_XOR:
- handleXORTrue(logicop, bexpr);
- break;
- case SATC_IMPLIES:
- handleIMPLIESTrue(logicop, bexpr);
- break;
- }
- }
+ replaceBooleanWithTrueNoRemove(bexpr);
}
-void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
- if (constraints.contains(oldb)) {
- constraints.remove(oldb);
- constraints.add(newb);
- }
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+ replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
- uint size = oldb->parents.getSize();
- for (uint i = 0; i < size; i++) {
- Boolean *parent = oldb->parents.get(i);
- BooleanLogic *logicop = (BooleanLogic *) parent;
+void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
+ updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
- uint parentsize = logicop->inputs.getSize();
+ ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
- for (uint j = 0; j < parentsize; j++) {
- Boolean *b = logicop->inputs.get(i);
- if (b == oldb) {
- logicop->inputs.set(i, newb);
- newb->parents.push(parent);
+ uint size = bexpr->parents.getSize();
+ for (uint i = 0; i < size; i++) {
+ ASTNode *parent = bexpr->parents.get(i);
+ if (parent->type == ELEMFUNCRETURN) {
+ ElementFunction *ef = (ElementFunction *) parent;
+ handleFunction(ef, bexpr);
+ } else {
+ ASSERT(parent->type == LOGICOP);
+ BooleanLogic *logicop = (BooleanLogic *) parent;
+ switch (logicop->op) {
+ case SATC_AND:
+ handleANDTrue(logicop, bexpr);
+ break;
+ case SATC_IFF:
+ handleIFFTrue(logicop, bexpr);
+ break;
+ case SATC_NOT:
+ case SATC_OR:
+ case SATC_XOR:
+ case SATC_IMPLIES:
+ ASSERT(0);
}
}
}
}
-void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
- uint size = bexpr->inputs.getSize();
- Boolean *b = bexpr->inputs.get(0);
- uint childindex = (b == child) ? 0 : 1;
- bexpr->inputs.remove(childindex);
- bexpr->op = SATC_NOT;
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
+ BooleanEdge childNegate = child.negate();
+ elemMap.remove(ef);
+ if (ef->overflowstatus == child) {
+ ef->overflowstatus = boolTrue;
+ } else if (ef->overflowstatus == childNegate) {
+ ef->overflowstatus = boolFalse;
+ }
+ elemMap.put(ef, ef);
}
-void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
- uint size = bexpr->inputs.getSize();
- Boolean *b = bexpr->inputs.get(0);
- uint otherindex = (b == child) ? 1 : 0;
- replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
-}
+void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
+ //Canonicalize
+ if (oldb.isNegated()) {
+ oldb = oldb.negate();
+ newb = newb.negate();
-void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
- uint size = bexpr->inputs.getSize();
- Boolean *b = bexpr->inputs.get(0);
- if (b == child) {
- //Replace with other term
- replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
- } else {
- //Statement is true...
- replaceBooleanWithTrue(bexpr);
}
-}
-
-void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
- uint size = bexpr->inputs.getSize();
- Boolean *b = bexpr->inputs.get(0);
- if (b == child) {
- //Statement is true...
- replaceBooleanWithTrue(bexpr);
- } else {
- //Make into negation of first term
- bexpr->inputs.get(1);
- bexpr->op = SATC_NOT;
+ if (constraints.contains(oldb)) {
+ constraints.remove(oldb);
+ constraints.add(newb);
+ if (newb->type == BOOLEANVAR)
+ replaceBooleanWithTrue(newb);
+ else
+ replaceBooleanWithTrueNoRemove(newb);
+ return;
}
-}
-
-void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
- uint size = bexpr->inputs.getSize();
-
- if (size == 1) {
- replaceBooleanWithTrue(bexpr);
+ if (constraints.contains(oldb.negate())) {
+ constraints.remove(oldb.negate());
+ constraints.add(newb.negate());
+ if (newb->type == BOOLEANVAR)
+ replaceBooleanWithTrue(newb.negate());
+ else
+ replaceBooleanWithTrueNoRemove(newb.negate());
return;
}
+ BooleanEdge oldbnegated = oldb.negate();
+ uint size = oldb->parents.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *b = bexpr->inputs.get(i);
- if (b == child) {
- bexpr->inputs.remove(i);
+ ASTNode *parent = oldb->parents.get(i);
+ if (parent->type == ELEMFUNCRETURN) {
+ ElementFunction *ef = (ElementFunction *) parent;
+ elemMap.remove(ef);
+ if (ef->overflowstatus == oldb) {
+ ef->overflowstatus = newb;
+ newb->parents.push(ef);
+ } else if (ef->overflowstatus == oldbnegated) {
+ ef->overflowstatus = newb.negate();
+ newb->parents.push(ef);
+ }
+ elemMap.put(ef, ef);
+ } else {
+ BooleanLogic *logicop = (BooleanLogic *) parent;
+ boolMap.remove(logicop); //could change parent's hash
+
+ uint parentsize = logicop->inputs.getSize();
+ for (uint j = 0; j < parentsize; j++) {
+ BooleanEdge b = logicop->inputs.get(j);
+ if (b == oldb) {
+ logicop->inputs.set(j, newb);
+ newb->parents.push(logicop);
+ } else if (b == oldbnegated) {
+ logicop->inputs.set(j, newb.negate());
+ newb->parents.push(logicop);
+ }
+ }
+ boolMap.put(logicop, logicop);
}
}
-
- if (size == 2) {
- replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
- }
}
-void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
uint size = bexpr->inputs.getSize();
+ BooleanEdge b0 = bexpr->inputs.get(0);
+ BooleanEdge b1 = bexpr->inputs.get(1);
+ BooleanEdge childnegate = child.negate();
+ bexpr->replaced = true;
+ if (b0 == child) {
+ replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
+ } else if (b0 == childnegate) {
+ replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
+ } else if (b1 == child) {
+ replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
+ } else if (b1 == childnegate) {
+ replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
+ } else
+ ASSERT(0);
+}
- if (size == 1) {
- replaceBooleanWithFalse(bexpr);
- }
+void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
+ BooleanEdge childNegate = child.negate();
+
+ boolMap.remove(bexpr);
+
+ for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
+ BooleanEdge b = bexpr->inputs.get(i);
- for (uint i = 0; i < size; i++) {
- Boolean *b = bexpr->inputs.get(i);
if (b == child) {
bexpr->inputs.remove(i);
+ i--;
+ } else if (b == childNegate) {
+ replaceBooleanWithFalse(bexpr);
+ return;
}
}
- if (size == 2) {
+ uint size = bexpr->inputs.getSize();
+ if (size == 0) {
+ bexpr->replaced = true;
+ replaceBooleanWithTrue(bexpr);
+ } else if (size == 1) {
+ bexpr->replaced = true;
replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
+ } else {
+ //Won't build any of these in future cases...
+ boolMap.put(bexpr, bexpr);
}
}
-void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
- if (constraints.contains(bexpr)) {
- setUnSAT();
- constraints.remove(bexpr);
- }
+void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
+ replaceBooleanWithTrue(bexpr.negate());
+}
- uint size = bexpr->parents.getSize();
- for (uint i = 0; i < size; i++) {
- Boolean *parent = bexpr->parents.get(i);
- BooleanLogic *logicop = (BooleanLogic *) parent;
- switch (logicop->op) {
- case SATC_AND:
- replaceBooleanWithFalse(parent);
- break;
- case SATC_OR:
- handleORFalse(logicop, bexpr);
- break;
- case SATC_NOT:
- replaceBooleanWithTrue(parent);
- break;
- case SATC_IFF:
- handleXORTrue(logicop, bexpr);
- break;
- case SATC_XOR:
- handleXORFalse(logicop, bexpr);
- break;
- case SATC_IMPLIES:
- handleIMPLIESFalse(logicop, bexpr);
- break;
- }
+BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
+ bool isNegated = bexpr.isNegated();
+ BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
+ BooleanEdge result;
+ if (b->op == SATC_IFF) {
+ if (isTrue(b->inputs.get(0))) {
+ result = b->inputs.get(1);
+ } else if (isFalse(b->inputs.get(0))) {
+ result = b->inputs.get(1).negate();
+ } else if (isTrue(b->inputs.get(1))) {
+ result = b->inputs.get(0);
+ } else if (isFalse(b->inputs.get(1))) {
+ result = b->inputs.get(0).negate();
+ } else ASSERT(0);
+ } else if (b->op == SATC_AND) {
+ uint size = b->inputs.getSize();
+ if (size == 0)
+ result = boolTrue;
+ else if (size == 1)
+ result = b->inputs.get(0);
+ else ASSERT(0);
}
+ return isNegated ? result.negate() : result;
}
projects / satune.git / blobdiff