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 dc69a575568a101132171a872b54673ccffa02c6..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();
@@ -24,7 +27,7 @@ void updateEdgePolarity(BooleanEdge dst, Polarity p) {
        Boolean *bdst = dst.getBoolean();
        bool isNegated = dst.isNegated();
        if (isNegated)
-               p=negatePolarity(p);
+               p = negatePolarity(p);
        updatePolarity(bdst, p);
 }
 
@@ -44,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);
@@ -59,8 +63,8 @@ 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);
+       for (uint i = 0; i < This->inputs.getSize(); i++) {
+               Element *e = This->inputs.get(i);
                computeElement(e);
        }
 }
@@ -73,10 +77,10 @@ void computeElement(Element *e) {
                        computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
                }
 
-               for(uint i=0; i < ef->inputs.getSize(); i++) {
-                       Element * echild = ef->inputs.get(i);
+               for (uint i = 0; i < ef->inputs.getSize(); i++) {
+                       Element *echild = ef->inputs.get(i);
                        computeElement(echild);
-               }       
+               }
        }
 }