Bug fix

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 0f9491a4c2277dd1565ae1911e572432f2a6e596..5d8865e466717f6625fba9242c5dc15c9b7355e2 100644 (file)
--- 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),
 BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) :
        Boolean(LOGICOP),
        op(_op),

+       replaced(false),

        inputs(array, asize) {
 }
 
        inputs(array, asize) {
 }
 

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index c943b0fff058f512a2c30b039b5c247d5ef938f1..41e9d5b536cc4c9cbb549a8cb335b5cfb1480322 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -75,6 +75,7 @@ public:
        Boolean *clone(CSolver *solver, CloneMap *map);
 
        LogicOp op;
        Boolean *clone(CSolver *solver, CloneMap *map);
 
        LogicOp op;

+       bool replaced;

        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };
        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index cfa41d57accba0c829c40077afb6ea41e127a92f..c49fcf5d2d5d0c2fcbe0acf1846737527330e07a 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -1,6 +1,7 @@
 #include "rewriter.h"
 #include "boolean.h"
 #include "csolver.h"
 #include "rewriter.h"
 #include "boolean.h"
 #include "csolver.h"

+#include "polarityassignment.h"

 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {


@@ -15,6 +16,8 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 }
        
 void CSolver::replaceBooleanWithTrueNoRemove(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);
        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();
        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) {
        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();
        
 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--;
        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;
                }
                        replaceBooleanWithFalse(bexpr);
                        return;
                }


@@ -107,12 +111,42 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 
        uint size=bexpr->inputs.getSize();
        if (size == 0) {
 
        uint size=bexpr->inputs.getSize();
        if (size == 0) {

+               bexpr->replaced = true;

                replaceBooleanWithTrue(bexpr);
        } else if (size == 1) {
                replaceBooleanWithTrue(bexpr);
        } else if (size == 1) {

+               bexpr->replaced = true;

                replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
                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());
 }
        }
 }
 
 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 956b6bf4936d035937f3a70b91cb67e4c191cef6..ea16b8043ca84619cd2804d24f43c007f0bedcac 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -250,6 +250,21 @@ static int ptrcompares(const void *p1, const void *p2) {
                return 1;
 }
 
                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) {
 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);
                                }
                                        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;
                        }
                }
                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];
                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;
                        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) {
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {

-       if (constraint == boolTrue)
+       if (isTrue(constraint))

                return;
                return;

-       else if (constraint == boolFalse)
+       else if (isFalse(constraint))

                setUnSAT();
        else {
                setUnSAT();
        else {

-               if (!constraint.isNegated() && constraint->type == LOGICOP) {
+               if (constraint->type == LOGICOP) {

                        BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
                        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;
                        }
                }
                                return;
                        }
                }

diff --git a/src/csolver.h b/src/csolver.h
index 3ff8509b369bbd13249e8d48eaaa945c8e362679..b53b77ba9b9b6ffd565aa1698bc43999cc4f3ffc 100644 (file)
--- 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);
 
        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;
 
        /** This is a vector of constraints that must be satisfied. */
        HashsetBooleanEdge constraints;