Handle optimizations for mustbetrue/mustbefalse automatically
authorbdemsky <bdemsky@uci.edu>
Sun, 3 Sep 2017 03:57:42 +0000 (20:57 -0700)
committerbdemsky <bdemsky@uci.edu>
Sun, 3 Sep 2017 03:57:42 +0000 (20:57 -0700)
src/AST/boolean.h
src/AST/rewriter.cc
src/csolver.cc
src/csolver.h

index 218fc50..c943b0f 100644 (file)
@@ -16,8 +16,8 @@ public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
        virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
-       virtual bool isTrue() {return false;}
-       virtual bool isFalse() {return false;}
+       virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
+       virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
index 80e1f1a..cfa41d5 100644 (file)
@@ -11,6 +11,10 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
                constraints.remove(bexpr);
        }
 
+       replaceBooleanWithTrueNoRemove(bexpr);
+}
+       
+void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
                Boolean *parent = bexpr->parents.get(i);
index ecc237e..956b6bf 100644 (file)
@@ -348,6 +348,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                        updateMustValue(ptr, BV_MUSTBEFALSE);
                else
                        updateMustValue(ptr, BV_MUSTBETRUE);
+               
+               if (ptr->boolVal == BV_UNSAT)
+                       setUnSAT();
+               
+               replaceBooleanWithTrueNoRemove(constraint);
+               constraint->parents.clear();
        }
 }
 
index 2875a9c..3ff8509 100644 (file)
@@ -134,6 +134,7 @@ public:
        SATEncoder *getSATEncoder() {return satEncoder;}
 
        void replaceBooleanWithTrue(BooleanEdge bexpr);
+       void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
        void replaceBooleanWithFalse(BooleanEdge bexpr);
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();