BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) :
Boolean(LOGICOP),
op(_op),
+ replaced(false),
inputs(array, asize) {
}
Boolean *clone(CSolver *solver, CloneMap *map);
LogicOp op;
+ bool replaced;
Array<BooleanEdge> inputs;
CMEMALLOC;
};
#include "rewriter.h"
#include "boolean.h"
#include "csolver.h"
+#include "polarityassignment.h"
void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
if (constraints.contains(bexpr.negate())) {
}
void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
+ updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
+
uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
Boolean *parent = bexpr->parents.get(i);
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) {
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);
if (b == child) {
bexpr->inputs.remove(i);
i--;
- }
-
- if (b == childNegate) {
+ } else if (b == childNegate) {
replaceBooleanWithFalse(bexpr);
return;
}
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(BooleanEdge bexpr) {
replaceBooleanWithTrue(bexpr.negate());
}
+
+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;
+}
return 1;
}
+BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
+ BooleanEdge newarray[asize];
+ memcpy(newarray, array, asize * sizeof(BooleanEdge));
+ for(uint i=0; i < asize; i++) {
+ BooleanEdge b=newarray[i];
+ if (b->type == LOGICOP) {
+ if (((BooleanLogic *) b.getBoolean())->replaced) {
+ newarray[i] = doRewrite(newarray[i]);
+ i--;//Check again
+ }
+ }
+ }
+ return applyLogicalOperation(op, newarray, asize);
+}
+
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
BooleanEdge newarray[asize];
switch (op) {
newarray[0] = array[1 - i];
return applyLogicalOperation(SATC_NOT, newarray, 1);
}
+ } else if (array[i]->type == LOGICOP) {
+ BooleanLogic *b =(BooleanLogic *)array[i].getBoolean();
+ if (b->replaced) {
+ return rewriteLogicalOperation(op, array, asize);
+ }
}
}
break;
uint newindex = 0;
for (uint i = 0; i < asize; i++) {
BooleanEdge b = array[i];
+ if (b->type == LOGICOP) {
+ if (((BooleanLogic *)b.getBoolean())->replaced)
+ return rewriteLogicalOperation(op, array, asize);
+ }
if (b->type == BOOLCONST) {
if (b->isTrue())
continue;
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (constraint == boolTrue)
+ if (isTrue(constraint))
return;
- else if (constraint == boolFalse)
+ else if (isFalse(constraint))
setUnSAT();
else {
- if (!constraint.isNegated() && constraint->type == LOGICOP) {
+ if (constraint->type == LOGICOP) {
BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
- if (b->op==SATC_AND) {
- for(uint i=0;i<b->inputs.getSize();i++) {
- addConstraint(b->inputs.get(i));
+ if (!constraint.isNegated()) {
+ if (b->op==SATC_AND) {
+ for(uint i=0;i<b->inputs.getSize();i++) {
+ addConstraint(b->inputs.get(i));
+ }
+ return;
}
+ }
+ if (b->replaced) {
+ addConstraint(doRewrite(constraint));
return;
}
}
void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
+ //These two functions are helpers if the client has a pointer to a
+ //Boolean object that we have since replaced
+ BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
+ BooleanEdge doRewrite(BooleanEdge b);
/** This is a vector of constraints that must be satisfied. */
HashsetBooleanEdge constraints;