edits

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 207b327bf693182d4d06a7ded3b4849aa913b367..1b5d24dea0b90e32f9ff7c26470cd424f332f5b1 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -21,7 +21,7 @@ public:
        virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
        Polarity polarity;
        BooleanValue boolVal;
-       Vector<Boolean *> parents;
+       Vector<ASTNode *> parents;
        virtual void updateParents() {}
        
        CMEMALLOC;

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 565187afc1ab5996f85be63b8a4c8a79790b2223..9642d9cedaf0e3050c816dbb73f957a64101f755 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -59,6 +59,8 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) {
 
 void ElementFunction::updateParents() {
        for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+       if (overflowstatus)
+               overflowstatus->parents.push(this);
 }
 
 Set *ElementFunction::getRange() {

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 804d9deec5fe844de74bd96382e0ea5316de3656..58ef96b05228d2eb36adcb97bcf351eb2a1d37ff 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -2,6 +2,7 @@
 #include "boolean.h"
 #include "csolver.h"
 #include "polarityassignment.h"
+#include "element.h"
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
@@ -26,25 +27,41 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 
        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()) {
@@ -74,22 +91,35 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        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);
        }
 }
 

diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index ef988dd3fb0fc5b10a265d4e90e26659da9c3f00..dc69a575568a101132171a872b54673ccffa02c6 100644 (file)
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -59,6 +59,25 @@ void computePredicatePolarity(BooleanPredicate *This) {
        if (This->undefStatus) {
                computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
        }
+       for(uint i=0; i < This->inputs.getSize(); i++) {
+               Element * e = This->inputs.get(i);
+               computeElement(e);
+       }
+}
+
+void computeElement(Element *e) {
+       if (e->type == ELEMFUNCRETURN) {
+               ElementFunction *ef = (ElementFunction *) e;
+
+               if (ef->overflowstatus) {
+                       computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
+               }
+
+               for(uint i=0; i < ef->inputs.getSize(); i++) {
+                       Element * echild = ef->inputs.get(i);
+                       computeElement(echild);
+               }       
+       }
 }
 
 void computeLogicOpPolarity(BooleanLogic *This) {

diff --git a/src/ASTAnalyses/Polarity/polarityassignment.h b/src/ASTAnalyses/Polarity/polarityassignment.h
index ce5096fd4b5b1b71cfc3fbc55c1518f8d7aa09d8..5cf345ca6ff1b22d299135e5805db190a842d324 100644 (file)
--- a/src/ASTAnalyses/Polarity/polarityassignment.h
+++ b/src/ASTAnalyses/Polarity/polarityassignment.h
@@ -12,12 +12,14 @@
 #include "common.h"
 #include "ops.h"
 #include "boolean.h"
+#include "element.h"
 
 void computePolarities(CSolver *This);
 bool updatePolarity(Boolean *This, Polarity polarity);
 void updateEdgePolarity(BooleanEdge dst, BooleanEdge src);
 void updateEdgePolarity(BooleanEdge dst, Polarity polarity);
 void updateMustValue(Boolean *This, BooleanValue value);
+void computeElement(Element *e);
 void computePolarity(Boolean *boolean, Polarity polarity);
 void computePredicatePolarity(BooleanPredicate *This);
 void computeLogicOpPolarity(BooleanLogic *boolean);

diff --git a/src/classes.h b/src/classes.h
index db98ab2c2edef8c1071ef7edf856ebc65b4bde5e..58f5a02be32f12674ac48ce34e963856bef4172d 100644 (file)
--- a/src/classes.h
+++ b/src/classes.h
@@ -27,6 +27,7 @@ class Transformer;
 class Set;
 class BooleanLogic;
 class Serializer;
+class ElementFunction;
 
 typedef uint64_t VarType;
 typedef unsigned int uint;

diff --git a/src/csolver.h b/src/csolver.h
index b84d3245801d801e1524876841d9d378c26e4f81..53e1901d101624c6296d45f3824be341bc6e7b0c 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -175,7 +175,8 @@ public:
 private:
        void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
        void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
-
+       void handleFunction(ElementFunction * ef, BooleanEdge child);
+       
        //These two functions are helpers if the client has a pointer to a
        //Boolean object that we have since replaced
        BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);