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 cfa41d57accba0c829c40077afb6ea41e127a92f..b6908e1f1dc1b7435b21fa637345492ad4f98971 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -1,6 +1,7 @@
 #include "rewriter.h"
 #include "boolean.h"
 #include "csolver.h"
+#include "polarityassignment.h"
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
@@ -15,9 +16,14 @@ 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:
@@ -40,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();
@@ -55,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);
        }
 }
 
@@ -76,6 +94,7 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
        BooleanEdge b0 = bexpr->inputs.get(0);
        BooleanEdge b1 = bexpr->inputs.get(1);
        BooleanEdge childnegate = child.negate();
+       bexpr->replaced = true;
        if (b0 == child) {
                replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
        } else if (b0 == childnegate) {
@@ -91,15 +110,15 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
        BooleanEdge childNegate=child.negate();
        
+       boolMap.remove(bexpr);
+       
        for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
                BooleanEdge b = bexpr->inputs.get(i);
                
                if (b == child) {
                        bexpr->inputs.remove(i);
                        i--;
-               }
-               
-               if (b == childNegate) {
+               } else if (b == childNegate) {
                        replaceBooleanWithFalse(bexpr);
                        return;
                }
@@ -107,12 +126,42 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 
        uint size=bexpr->inputs.getSize();
        if (size == 0) {
+               bexpr->replaced = true;
                replaceBooleanWithTrue(bexpr);
        } else if (size == 1) {
+               bexpr->replaced = true;
                replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
+       } else {
+               //Won't build any of these in future cases...
+               boolMap.put(bexpr, bexpr);
        }
 }
 
 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
        replaceBooleanWithTrue(bexpr.negate());
 }
+
+BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
+       bool isNegated=bexpr.isNegated();
+       BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+       BooleanEdge result;
+       if (b->op == SATC_IFF) {
+               if (isTrue(b->inputs.get(0))) {
+                       result = b->inputs.get(1);
+               } else if (isFalse(b->inputs.get(0))) {
+                       result = b->inputs.get(1).negate();
+               } else if (isTrue(b->inputs.get(1))) {
+                       result = b->inputs.get(0);
+               } else if (isFalse(b->inputs.get(1))) {
+                       result = b->inputs.get(0).negate();
+               } else ASSERT(0);
+       } else if (b->op==SATC_AND) {
+               uint size = b->inputs.getSize();
+               if (size == 0)
+                       result = boolTrue;
+               else if (size == 1)
+                       result = b->inputs.get(0);
+               else ASSERT(0);
+       }
+       return isNegated ? result.negate() : result;
+}