Small edit

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

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index bf787ea3960b33d16fb90a01aa46fb16e1eed468..14789304b49a797d74a14e4da5af02b6008dcd76 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -2,14 +2,14 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-       HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
-       while(hasNextBoolean(iterator)) {
-               Boolean *boolean = nextBoolean(iterator);
+       SetIteratorBoolean *iterator = This->getConstraints();
+       while (iterator->hasNext()) {
+               Boolean *boolean = iterator->next();
                updatePolarity(boolean, P_TRUE);
                updateMustValue(boolean, BV_MUSTBETRUE);
                computePolarityAndBooleanValue(boolean);
        }
-       deleteIterBoolean(iterator);
+       delete iterator;
 }
 
 void updatePolarity(Boolean *This, Polarity polarity) {
@@ -21,7 +21,7 @@ void updateMustValue(Boolean *This, BooleanValue value) {
 }
 
 void computePolarityAndBooleanValue(Boolean *This) {
-       switch (GETBOOLEANTYPE(This)) {
+       switch (This->type) {
        case BOOLEANVAR:
        case ORDERCONST:
                return;
@@ -44,9 +44,9 @@ void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
        computeLogicOpBooleanValue(This);
        computeLogicOpPolarity(This);
-       uint size = getSizeArrayBoolean(&This->inputs);
+       uint size = This->inputs.getSize();
        for (uint i = 0; i < size; i++) {
-               computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
+               computePolarityAndBooleanValue(This->inputs.get(i));
        }
 }
 
@@ -79,31 +79,32 @@ BooleanValue negateBooleanValue(BooleanValue This) {
 }
 
 void computeLogicOpPolarity(BooleanLogic *This) {
-       Polarity parentpolarity = GETBOOLEANPOLARITY(This);
+       Polarity parentpolarity = This->polarity;
        switch (This->op) {
-       case L_AND:
-       case L_OR: {
-               uint size = getSizeArrayBoolean(&This->inputs);
+       case SATC_AND:
+       case SATC_OR: {
+               uint size = This->inputs.getSize();
                for (uint i = 0; i < size; i++) {
-                       Boolean *tmp = getArrayBoolean(&This->inputs, i);
+                       Boolean *tmp = This->inputs.get(i);
                        updatePolarity(tmp, parentpolarity);
                }
                break;
        }
-       case L_NOT: {
-               Boolean *tmp = getArrayBoolean(&This->inputs, 0);
+       case SATC_NOT: {
+               Boolean *tmp = This->inputs.get(0);
                updatePolarity(tmp, negatePolarity(parentpolarity));
                break;
        }
-       case L_XOR: {
-               updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
-               updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
+       case SATC_IFF:
+       case SATC_XOR: {
+               updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
+               updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
                break;
        }
-       case L_IMPLIES: {
-               Boolean *left = getArrayBoolean(&This->inputs, 0);
+       case SATC_IMPLIES: {
+               Boolean *left = This->inputs.get(0);
                updatePolarity(left, negatePolarity( parentpolarity));
-               Boolean *right = getArrayBoolean(&This->inputs, 1);
+               Boolean *right = This->inputs.get(1);
                updatePolarity(right, parentpolarity);
                break;
        }
@@ -113,38 +114,39 @@ void computeLogicOpPolarity(BooleanLogic *This) {
 }
 
 void computeLogicOpBooleanValue(BooleanLogic *This) {
-       BooleanValue parentbv = GETBOOLEANVALUE(This);
+       BooleanValue parentbv = This->boolVal;
        switch (This->op) {
-       case L_AND: {
+       case SATC_AND: {
                if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
-                       uint size = getSizeArrayBoolean(&This->inputs);
+                       uint size = This->inputs.getSize();
                        for (uint i = 0; i < size; i++) {
-                               updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+                               updateMustValue(This->inputs.get(i), parentbv);
                        }
                }
                return;
        }
-       case L_OR: {
+       case SATC_OR: {
                if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = getSizeArrayBoolean(&This->inputs);
+                       uint size = This->inputs.getSize();
                        for (uint i = 0; i < size; i++) {
-                               updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+                               updateMustValue(This->inputs.get(i), parentbv);
                        }
                }
                return;
        }
-       case L_NOT:
-               updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+       case SATC_NOT:
+               updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
                return;
-       case L_IMPLIES:
+       case SATC_IMPLIES:
                //implies is really an or with the first term negated
                if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = getSizeArrayBoolean(&This->inputs);
-                       updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
-                       updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
+                       uint size = This->inputs.getSize();
+                       updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
+                       updateMustValue(This->inputs.get(1), parentbv);
                }
                return;
-       case L_XOR:
+       case SATC_IFF:
+       case SATC_XOR:
                return;
        default:
                ASSERT(0);