Compute Must Values Automatically

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

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index f0dac379af4dbb999370f5a35dd0099970393956..f75c9ece2b11f5178c39e3ac4dbfc2c79a145824 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -2,12 +2,17 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-       HSIteratorBoolean *iterator = This->getConstraints();
+       SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
-               Boolean *boolean = iterator->next();
-               updatePolarity(boolean, P_TRUE);
-               updateMustValue(boolean, BV_MUSTBETRUE);
-               computePolarityAndBooleanValue(boolean);
+               BooleanEdge boolean = iterator->next();
+               Boolean *b = boolean.getBoolean();
+               bool isNegated = boolean.isNegated();
+               if (isNegated) {
+                       updatePolarity(b, P_FALSE);
+               } else {
+                       updatePolarity(b, P_TRUE);
+               }
+               computePolarity(b);
        }
        delete iterator;
 }
@@ -20,33 +25,32 @@ void updateMustValue(Boolean *This, BooleanValue value) {
        This->boolVal = (BooleanValue) (This->boolVal | value);
 }
 
-void computePolarityAndBooleanValue(Boolean *This) {
+void computePolarity(Boolean *This) {
        switch (This->type) {
        case BOOLEANVAR:
        case ORDERCONST:
                return;
        case PREDICATEOP:
-               return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
+               return computePredicatePolarity((BooleanPredicate *)This);
        case LOGICOP:
-               return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
+               return computeLogicOpPolarity((BooleanLogic *)This);
        default:
                ASSERT(0);
        }
 }
 
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
-       if (This->undefStatus != NULL) {
-               updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
-               computePolarityAndBooleanValue(This->undefStatus);
+void computePredicatePolarity(BooleanPredicate *This) {
+       if (This->undefStatus) {
+               updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
+               computePolarity(This->undefStatus.getBoolean());
        }
 }
 
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
-       computeLogicOpBooleanValue(This);
-       computeLogicOpPolarity(This);
+void computeLogicOpPolarity(BooleanLogic *This) {
+       computeLogicOpPolarityChildren(This);
        uint size = This->inputs.getSize();
        for (uint i = 0; i < size; i++) {
-               computePolarityAndBooleanValue(This->inputs.get(i));
+               computePolarity(This->inputs.get(i).getBoolean());
        }
 }
 
@@ -78,74 +82,23 @@ BooleanValue negateBooleanValue(BooleanValue This) {
        }
 }
 
-void computeLogicOpPolarity(BooleanLogic *This) {
+void computeLogicOpPolarityChildren(BooleanLogic *This) {
        Polarity parentpolarity = This->polarity;
        switch (This->op) {
-       case SATC_AND:
-       case SATC_OR: {
+       case SATC_AND: {
                uint size = This->inputs.getSize();
                for (uint i = 0; i < size; i++) {
-                       Boolean *tmp = This->inputs.get(i);
-                       updatePolarity(tmp, parentpolarity);
+                       BooleanEdge tmp = This->inputs.get(i);
+                       Boolean *btmp = tmp.getBoolean();
+                       updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
                }
                break;
        }
-       case SATC_NOT: {
-               Boolean *tmp = This->inputs.get(0);
-               updatePolarity(tmp, negatePolarity(parentpolarity));
+       case SATC_IFF: {
+               updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
+               updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
                break;
        }
-       case SATC_XOR: {
-               updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
-               updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
-               break;
-       }
-       case SATC_IMPLIES: {
-               Boolean *left = This->inputs.get(0);
-               updatePolarity(left, negatePolarity( parentpolarity));
-               Boolean *right = This->inputs.get(1);
-               updatePolarity(right, parentpolarity);
-               break;
-       }
-       default:
-               ASSERT(0);
-       }
-}
-
-void computeLogicOpBooleanValue(BooleanLogic *This) {
-       BooleanValue parentbv = This->boolVal;
-       switch (This->op) {
-       case SATC_AND: {
-               if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
-                       uint size = This->inputs.getSize();
-                       for (uint i = 0; i < size; i++) {
-                               updateMustValue(This->inputs.get(i), parentbv);
-                       }
-               }
-               return;
-       }
-       case SATC_OR: {
-               if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = This->inputs.getSize();
-                       for (uint i = 0; i < size; i++) {
-                               updateMustValue(This->inputs.get(i), parentbv);
-                       }
-               }
-               return;
-       }
-       case SATC_NOT:
-               updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
-               return;
-       case SATC_IMPLIES:
-               //implies is really an or with the first term negated
-               if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = This->inputs.getSize();
-                       updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
-                       updateMustValue(This->inputs.get(1), parentbv);
-               }
-               return;
-       case SATC_XOR:
-               return;
        default:
                ASSERT(0);
        }