Handle optimizations for mustbetrue/mustbefalse automatically

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 218fc501dab56b41e4fc7f1cb1258406a304b6a7..c943b0fff058f512a2c30b039b5c247d5ef938f1 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -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;

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 80e1f1a90d4b34085527de89e2fdd678949ac2fc..cfa41d57accba0c829c40077afb6ea41e127a92f 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -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);

diff --git a/src/csolver.cc b/src/csolver.cc
index ecc237e59b7c680411e66aef6757b774beee8f20..956b6bf4936d035937f3a70b91cb67e4c191cef6 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -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();
        }
 }
 

diff --git a/src/csolver.h b/src/csolver.h
index 2875a9c78365e708912ddcd5ef2620837212af66..3ff8509b369bbd13249e8d48eaaa945c8e362679 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -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();