Improve propagation and add preprocessor pass

[satune.git] / src / AST / rewriter.cc

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index c49fcf5d2d5d0c2fcbe0acf1846737527330e07a..b6908e1f1dc1b7435b21fa637345492ad4f98971 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -17,10 +17,13 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
+
+       ASSERT(bexpr->boolVal != BV_UNSAT);
        
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
                Boolean *parent = bexpr->parents.get(i);
+               ASSERT(parent->type == LOGICOP);
                BooleanLogic *logicop = (BooleanLogic *) parent;
                switch (logicop->op) {
                case SATC_AND:
@@ -43,14 +46,25 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        if (oldb.isNegated()) {
                oldb=oldb.negate();
                newb=newb.negate();
+
        }
        if (constraints.contains(oldb)) {
                constraints.remove(oldb);
                constraints.add(newb);
+               if (newb->type == BOOLEANVAR)
+                       replaceBooleanWithTrue(newb);
+               else
+                       replaceBooleanWithTrueNoRemove(newb);
+               return;
        }
        if (constraints.contains(oldb.negate())) {
                constraints.remove(oldb.negate());
                constraints.add(newb.negate());
+               if (newb->type == BOOLEANVAR)
+                       replaceBooleanWithTrue(newb.negate());
+               else
+                       replaceBooleanWithTrueNoRemove(newb.negate());
+               return;
        }
 
        BooleanEdge oldbnegated = oldb.negate();
@@ -58,19 +72,20 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        for (uint i = 0; i < size; i++) {
                Boolean *parent = oldb->parents.get(i);
                BooleanLogic *logicop = (BooleanLogic *) parent;
-
+               boolMap.remove(parent); //could change parent's hash
+               
                uint parentsize = logicop->inputs.getSize();
-
                for (uint j = 0; j < parentsize; j++) {
-                       BooleanEdge b = logicop->inputs.get(i);
+                       BooleanEdge b = logicop->inputs.get(j);
                        if (b == oldb) {
-                               logicop->inputs.set(i, newb);
+                               logicop->inputs.set(j, newb);
                                newb->parents.push(parent);
                        } else if (b == oldbnegated) {
-                               logicop->inputs.set(i, newb.negate());
+                               logicop->inputs.set(j, newb.negate());
                                newb->parents.push(parent);
                        }
                }
+               boolMap.put(parent, parent);
        }
 }