Bug fix

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index dcc201d24c319ee324eb63a484e39239049c2633..939f937d37fa4b02e516cb6f75920cf7a110b0e2 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -96,6 +96,8 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
 
 void BooleanPredicate::updateParents() {
        for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+       if (undefStatus)
+               undefStatus->parents.push(this);
 }
 
 void BooleanLogic::updateParents() {

diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 7a8104dcd4453e6994c6fee547e50d0d488028e7..b0ff8198c7d5e11a75beaaff5742c1c267ee1285 100644 (file)
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -20,7 +20,9 @@ public:
        Boolean *getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
        Boolean *getRaw() {return b;}
        Boolean *operator->() {return getBoolean();}
-       operator bool() const {return b != NULL;}
+       operator bool() {
+               return getBoolean() != NULL;
+       }
 private:
        Boolean *b;
 };

diff --git a/src/csolver.cc b/src/csolver.cc
index be4a3a88063882cc05f5cfafca9218724b870f72..a2163a0c839103179fc6a31df3608ea71651d8a9 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -65,7 +65,6 @@ CSolver::~CSolver() {
        for (uint i = 0; i < size; i++) {
                delete allOrders.get(i);
        }
-
        size = allFunctions.getSize();
        for (uint i = 0; i < size; i++) {
                delete allFunctions.get(i);
@@ -103,7 +102,6 @@ void CSolver::serialize() {
                Deserializer deserializer("dump");
                deserializer.deserialize();
        }
-
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -175,6 +173,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
        }
 }
 
+
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
        Element *e = elemMap.get(element);
@@ -311,13 +310,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        }
        case SATC_IFF: {
                for (uint i = 0; i < 2; i++) {
-                       if (array[i]->type == BOOLCONST) {
-                               if (isTrue(array[i])) { // It can be undefined
-                                       return array[1 - i];
-                               } else if (isFalse(array[i])) {
-                                       newarray[0] = array[1 - i];
-                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
-                               }
+                       if (isTrue(array[i])) { // It can be undefined
+                               return array[1 - i];
+                       } else if (isFalse(array[i])) {
+                               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) {
@@ -341,12 +338,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                                if (((BooleanLogic *)b.getBoolean())->replaced)
                                        return rewriteLogicalOperation(op, array, asize);
                        }
-                       if (b->type == BOOLCONST) {
-                               if (isTrue(b))
-                                       continue;
-                               else {
-                                       return boolFalse;
-                               }
+                       if (isTrue(b))
+                               continue;
+                       else if (isFalse(b)) {
+                               return boolFalse;
                        } else
                                newarray[newindex++] = b;
                }
@@ -389,7 +384,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
        //      ASSERT(first != second);
        if (first == second)
                return getBooleanFalse();
-       
+
        bool negate = false;
        if (order->type == SATC_TOTAL) {
                if (first > second) {