Compute Must Values Automatically

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 6b634361a3f0727fa1ac1b86163cb905c7e71f5f..f75c9ece2b11f5178c39e3ac4dbfc2c79a145824 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -9,12 +9,10 @@ void computePolarities(CSolver *This) {
                bool isNegated = boolean.isNegated();
                if (isNegated) {
                        updatePolarity(b, P_FALSE);
-                       updateMustValue(b, BV_MUSTBEFALSE);
                } else {
                        updatePolarity(b, P_TRUE);
-                       updateMustValue(b, BV_MUSTBETRUE);
                }
-               computePolarityAndBooleanValue(b);
+               computePolarity(b);
        }
        delete iterator;
 }
@@ -27,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) {
+void computePredicatePolarity(BooleanPredicate *This) {
        if (This->undefStatus) {
                updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
-               computePolarityAndBooleanValue(This->undefStatus.getBoolean());
+               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).getBoolean());
+               computePolarity(This->inputs.get(i).getBoolean());
        }
 }
 
@@ -85,7 +82,7 @@ BooleanValue negateBooleanValue(BooleanValue This) {
        }
 }
 
-void computeLogicOpPolarity(BooleanLogic *This) {
+void computeLogicOpPolarityChildren(BooleanLogic *This) {
        Polarity parentpolarity = This->polarity;
        switch (This->op) {
        case SATC_AND: {
@@ -106,23 +103,3 @@ void computeLogicOpPolarity(BooleanLogic *This) {
                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++) {
-                               BooleanEdge be=This->inputs.get(i);
-                               updateMustValue(be.getBoolean(), be.isNegated()?negateBooleanValue(parentbv):parentbv);
-                       }
-               }
-               return;
-       }
-       case SATC_IFF:
-               return;
-       default:
-               ASSERT(0);
-       }
-}

diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h
index 6621d773617b228b1c0a39afb71b4662bde54364..625587543b2e86131320baab2b4da189c365fec0 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.h
+++ b/src/ASTAnalyses/polarityassignment.h
@@ -16,12 +16,11 @@
 void computePolarities(CSolver *This);
 void updatePolarity(Boolean *This, Polarity polarity);
 void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarityAndBooleanValue(Boolean *boolean);
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
+void computePolarity(Boolean *boolean);
+void computePredicatePolarity(BooleanPredicate *This);
+void computeLogicOpPolarity(BooleanLogic *boolean);
 Polarity negatePolarity(Polarity This);
 BooleanValue negateBooleanValue(BooleanValue This);
-void computeLogicOpPolarity(BooleanLogic *boolean);
-void computeLogicOpBooleanValue(BooleanLogic *boolean);
+void computeLogicOpPolarityChildren(BooleanLogic *boolean);
 
 #endif/* POLARITYASSIGNMENT_H */

diff --git a/src/csolver.cc b/src/csolver.cc
index 3e240a4df2741050576d1cf00cc3a6f639f5bb54..ecc237e59b7c680411e66aef6757b774beee8f20 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -342,8 +342,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                                return;
                        }
                }
-
                constraints.add(constraint);
+               Boolean *ptr=constraint.getBoolean();
+               if (constraint.isNegated())
+                       updateMustValue(ptr, BV_MUSTBEFALSE);
+               else
+                       updateMustValue(ptr, BV_MUSTBETRUE);
        }
 }