From da9bf180de81b31c95fb4987b84412e11ce3f6eb Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sun, 3 Sep 2017 22:48:18 -0700 Subject: [PATCH 1/1] Bug fix --- src/AST/boolean.cc | 1 + src/AST/boolean.h | 1 + src/AST/rewriter.cc | 40 +++++++++++++++++++++++++++++++++++++--- src/csolver.cc | 42 ++++++++++++++++++++++++++++++++++++------ src/csolver.h | 4 ++++ 5 files changed, 79 insertions(+), 9 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 0f9491a..5d8865e 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -45,6 +45,7 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) : Boolean(LOGICOP), op(_op), + replaced(false), inputs(array, asize) { } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index c943b0f..41e9d5b 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -75,6 +75,7 @@ public: Boolean *clone(CSolver *solver, CloneMap *map); LogicOp op; + bool replaced; Array inputs; CMEMALLOC; }; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index cfa41d5..c49fcf5 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -1,6 +1,7 @@ #include "rewriter.h" #include "boolean.h" #include "csolver.h" +#include "polarityassignment.h" void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) { if (constraints.contains(bexpr.negate())) { @@ -15,6 +16,8 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) { } 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); @@ -76,6 +79,7 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) { 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) { @@ -91,15 +95,15 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) { 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; } @@ -107,12 +111,42 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) { 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; +} diff --git a/src/csolver.cc b/src/csolver.cc index 956b6bf..ea16b80 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -250,6 +250,21 @@ static int ptrcompares(const void *p1, const void *p2) { 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) { @@ -265,6 +280,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint 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; @@ -279,6 +299,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint 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; @@ -328,17 +352,23 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } 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;iinputs.getSize();i++) { - addConstraint(b->inputs.get(i)); + if (!constraint.isNegated()) { + if (b->op==SATC_AND) { + for(uint i=0;iinputs.getSize();i++) { + addConstraint(b->inputs.get(i)); + } + return; } + } + if (b->replaced) { + addConstraint(doRewrite(constraint)); return; } } diff --git a/src/csolver.h b/src/csolver.h index 3ff8509..b53b77b 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -151,6 +151,10 @@ private: 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; -- 2.34.1