Bug fix
authorbdemsky <bdemsky@uci.edu>
Mon, 4 Sep 2017 05:48:18 +0000 (22:48 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 4 Sep 2017 05:48:18 +0000 (22:48 -0700)
src/AST/boolean.cc
src/AST/boolean.h
src/AST/rewriter.cc
src/csolver.cc
src/csolver.h

index 0f9491a..5d8865e 100644 (file)
@@ -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) {
 }
 
index c943b0f..41e9d5b 100644 (file)
@@ -75,6 +75,7 @@ public:
        Boolean *clone(CSolver *solver, CloneMap *map);
 
        LogicOp op;
+       bool replaced;
        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };
index cfa41d5..c49fcf5 100644 (file)
@@ -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;
+}
index 956b6bf..ea16b80 100644 (file)
@@ -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;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;
                        }
                }
index 3ff8509..b53b77b 100644 (file)
@@ -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;