Merge
authorbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 22:12:22 +0000 (15:12 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 22:12:22 +0000 (15:12 -0700)
src/AST/boolean.cc
src/Collections/corestructs.h
src/csolver.cc

index dcc201d..939f937 100644 (file)
@@ -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() {
index 7a8104d..b0ff819 100644 (file)
@@ -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;
 };
index d316724..71205f6 100644 (file)
@@ -66,7 +66,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);
@@ -175,6 +174,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 +311,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 +339,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 +385,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) {
@@ -510,7 +506,6 @@ void CSolver::printConstraints() {
                model_print("\n");
        }
        delete it;
-
 }
 
 void CSolver::printConstraint(BooleanEdge b) {