bug fix

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

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 937a8b74cb442f2f6a0738fa039da845a0558eb8..fef4dcbb17aaf40626791272a67db9d68cf0de11 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -2,77 +2,124 @@
 #include "boolean.h"
 #include "csolver.h"
 #include "polarityassignment.h"
+#include "element.h"
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
                constraints.remove(bexpr.negate());
                setUnSAT();
-       }       
+       }
        if (constraints.contains(bexpr)) {
                constraints.remove(bexpr);
        }
 
        replaceBooleanWithTrueNoRemove(bexpr);
 }
-       
+
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+       replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
+
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
-       
+
+       ASSERT((bexpr->boolVal != BV_UNSAT ) || 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:
-                       handleANDTrue(logicop, bexpr);
-                       break;
-               case SATC_IFF:
-                       handleIFFTrue(logicop, bexpr);
-                       break;
-               case SATC_NOT:
-               case SATC_OR:
-               case SATC_XOR:
-               case SATC_IMPLIES:
-                       ASSERT(0);
+               ASTNode *parent = bexpr->parents.get(i);
+               if (parent->type == ELEMFUNCRETURN) {
+                       ElementFunction *ef = (ElementFunction *) parent;
+                       handleFunction(ef, bexpr);
+               } else {
+                       ASSERT(parent->type == LOGICOP);
+                       BooleanLogic *logicop = (BooleanLogic *) parent;
+                       switch (logicop->op) {
+                       case SATC_AND:
+                               handleANDTrue(logicop, bexpr);
+                               break;
+                       case SATC_IFF:
+                               handleIFFTrue(logicop, bexpr);
+                               break;
+                       case SATC_NOT:
+                       case SATC_OR:
+                       case SATC_XOR:
+                       case SATC_IMPLIES:
+                               ASSERT(0);
+                       }
                }
        }
 }
 
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
+       BooleanEdge childNegate = child.negate();
+       elemMap.remove(ef);
+       if (ef->overflowstatus == child) {
+               ef->overflowstatus = boolTrue;
+       } else if (ef->overflowstatus == childNegate) {
+               ef->overflowstatus = boolFalse;
+       }
+       elemMap.put(ef, ef);
+}
+
 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        //Canonicalize
        if (oldb.isNegated()) {
-               oldb=oldb.negate();
-               newb=newb.negate();
+               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();
        uint size = oldb->parents.getSize();
        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(j);
-                       if (b == oldb) {
-                               logicop->inputs.set(j, newb);
-                               newb->parents.push(parent);
-                       } else if (b == oldbnegated) {
-                               logicop->inputs.set(j, newb.negate());
-                               newb->parents.push(parent);
+               ASTNode *parent = oldb->parents.get(i);
+               if (parent->type == ELEMFUNCRETURN) {
+                       ElementFunction *ef = (ElementFunction *) parent;
+                       elemMap.remove(ef);
+                       if (ef->overflowstatus == oldb) {
+                               ef->overflowstatus = newb;
+                               newb->parents.push(ef);
+                       } else if (ef->overflowstatus == oldbnegated) {
+                               ef->overflowstatus = newb.negate();
+                               newb->parents.push(ef);
+                       }
+                       elemMap.put(ef, ef);
+               } else {
+                       BooleanLogic *logicop = (BooleanLogic *) parent;
+                       boolMap.remove(logicop);        //could change parent's hash
+
+                       uint parentsize = logicop->inputs.getSize();
+                       for (uint j = 0; j < parentsize; j++) {
+                               BooleanEdge b = logicop->inputs.get(j);
+                               if (b == oldb) {
+                                       logicop->inputs.set(j, newb);
+                                       newb->parents.push(logicop);
+                               } else if (b == oldbnegated) {
+                                       logicop->inputs.set(j, newb.negate());
+                                       newb->parents.push(logicop);
+                               }
                        }
+                       boolMap.put(logicop, logicop);
                }
-               boolMap.put(parent, parent);
        }
 }
 
@@ -95,13 +142,13 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 }
 
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
-       BooleanEdge childNegate=child.negate();
-       
+       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--;
@@ -111,7 +158,7 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
                }
        }
 
-       uint size=bexpr->inputs.getSize();
+       uint size = bexpr->inputs.getSize();
        if (size == 0) {
                bexpr->replaced = true;
                replaceBooleanWithTrue(bexpr);
@@ -129,8 +176,8 @@ void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 }
 
 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
-       bool isNegated=bexpr.isNegated();
-       BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+       bool isNegated = bexpr.isNegated();
+       BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
        BooleanEdge result;
        if (b->op == SATC_IFF) {
                if (isTrue(b->inputs.get(0))) {
@@ -142,7 +189,7 @@ BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
                } else if (isFalse(b->inputs.get(1))) {
                        result = b->inputs.get(0).negate();
                } else ASSERT(0);
-       } else if (b->op==SATC_AND) {
+       } else if (b->op == SATC_AND) {
                uint size = b->inputs.getSize();
                if (size == 0)
                        result = boolTrue;