Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / ASTAnalyses / Polarity / polarityassignment.cc

diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index 6254832477b7abd72102e544e2d75012a026f671..b8b01d0e6a4b99f769a4df47d7fa734c044a5f10 100644 (file)
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -2,6 +2,9 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
+       if(This->isUnSAT()){
+               return;
+       }
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge boolean = iterator->next();
@@ -12,6 +15,22 @@ void computePolarities(CSolver *This) {
        delete iterator;
 }
 
+void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
+       Boolean *bdst = dst.getBoolean();
+       Boolean *bsrc = src.getBoolean();
+       bool isNegated = dst.isNegated() ^ src.isNegated();
+       Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
+       updatePolarity(bdst, p);
+}
+
+void updateEdgePolarity(BooleanEdge dst, Polarity p) {
+       Boolean *bdst = dst.getBoolean();
+       bool isNegated = dst.isNegated();
+       if (isNegated)
+               p = negatePolarity(p);
+       updatePolarity(bdst, p);
+}
+
 bool updatePolarity(Boolean *This, Polarity polarity) {
        Polarity oldpolarity = This->polarity;
        Polarity newpolarity = (Polarity) (This->polarity | polarity);
@@ -28,6 +47,7 @@ void computePolarity(Boolean *This, Polarity polarity) {
                switch (This->type) {
                case BOOLEANVAR:
                case ORDERCONST:
+               case BOOLCONST:
                        return;
                case PREDICATEOP:
                        return computePredicatePolarity((BooleanPredicate *)This);
@@ -43,6 +63,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) {
@@ -54,20 +93,6 @@ void computeLogicOpPolarity(BooleanLogic *This) {
        }
 }
 
-Polarity negatePolarity(Polarity This) {
-       switch (This) {
-       case P_UNDEFINED:
-       case P_BOTHTRUEFALSE:
-               return This;
-       case P_TRUE:
-               return P_FALSE;
-       case P_FALSE:
-               return P_TRUE;
-       default:
-               ASSERT(0);
-       }
-}
-
 BooleanValue negateBooleanValue(BooleanValue This) {
        switch (This) {
        case BV_UNDEFINED:
@@ -94,3 +119,17 @@ Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
                ASSERT(0);
        }
 }
+
+Polarity negatePolarity(Polarity This) {
+       switch (This) {
+       case P_UNDEFINED:
+       case P_BOTHTRUEFALSE:
+               return This;
+       case P_TRUE:
+               return P_FALSE;
+       case P_FALSE:
+               return P_TRUE;
+       default:
+               ASSERT(0);
+       }
+}