Clean up polarity pass

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 09ec2ae817de133940927287c7e68d65fe0427f7..591bfe61ac0a8de6a56c6ef2b6943914f3675349 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -76,33 +76,3 @@ void deleteBoolean(Boolean * This) {
        deleteVectorArrayBoolean(GETBOOLEANPARENTS(This));
        ourfree(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:
-               case BV_UNKNOWN:
-                       return This;
-               case BV_MUSTBETRUE:
-                       return BV_MUSTBEFALSE;
-               case BV_MUSTBEFALSE:
-                       return BV_MUSTBETRUE;
-               default:
-                       ASSERT(0);
-       }
-}
-

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index b24fa3f83e10d9cf093b6478bb515e7710507317..2a80d390820ac986f3c5918bb48932ec3e87a3b9 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -56,8 +56,6 @@ Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
 void deleteBoolean(Boolean * This);
-Polarity negatePolarity(Polarity This);
-BooleanValue negateBooleanValue(BooleanValue This);
 static inline FunctionEncoding* getPredicateFunctionEncoding(BooleanPredicate* func){
        return &func->encoding;
 }

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 9e8113d685ce48bd0e3f8dab0b7e38b1823d3c4b..c9de82de78db1aaabb70b48d50c90a4c668d2922 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -38,10 +38,10 @@ typedef enum PredicateType PredicateType;
 enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
 typedef enum ASTNodeType ASTNodeType;
 
-enum Polarity {P_UNDEFINED, P_TRUE, P_FALSE, P_BOTHTRUEFALSE};
+enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
 typedef enum Polarity Polarity;
 
-enum BooleanValue {BV_UNDEFINED, BV_MUSTBETRUE, BV_MUSTBEFALSE, BV_UNKNOWN};
+enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
 typedef enum BooleanValue BooleanValue;
 
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 3baada358e4ba904efe62e36acb9a911463a0376..bc64cc44f3a25777492142befd7570e44aec49fb 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -11,14 +11,12 @@
 #include "table.h"
 #include "tableentry.h"
 #include "order.h"
-#include "polarityassignment.h"
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver* This) {
        for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
                Boolean* boolean = getVectorBoolean(This->constraints, i);
                naiveEncodingConstraint(boolean);
-               assignPolarityAndBooleanValue(boolean);
        }
 }
 

diff --git a/src/Encoders/polarityassignment.c b/src/Encoders/polarityassignment.c
index 840df1b777cd78f18a25b87265a40e5339bf34c8..0ad5f8839415162ae53f756b837077253d122455 100644 (file)
--- a/src/Encoders/polarityassignment.c
+++ b/src/Encoders/polarityassignment.c
@@ -1,168 +1,148 @@
 #include "polarityassignment.h"
+#include "csolver.h"
 
-void assignPolarityAndBooleanValue(Boolean* boolean){
-       GETBOOLEANPOLARITY(boolean) = P_TRUE;
-       GETBOOLEANVALUE(boolean) = BV_MUSTBETRUE;
-       computePolarityAndBooleanValue(boolean);
+void computePolarities(CSolver* This) {
+       for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
+               Boolean* boolean = getVectorBoolean(This->constraints, i);
+               updatePolarity(boolean, P_TRUE);
+               updateMustValue(boolean, BV_MUSTBETRUE);
+               computePolarityAndBooleanValue(boolean);
+       }
+}
+
+void updatePolarity(Boolean *This, Polarity polarity) {
+       This->polarity |= polarity;
 }
 
-void computePolarityAndBooleanValue(Boolean* boolean){
-       switch( GETBOOLEANTYPE(boolean)){
+void updateMustValue(Boolean *This, BooleanValue value) {
+       This->boolVal |= value;
+}
+
+void computePolarityAndBooleanValue(Boolean* This) {
+       switch(GETBOOLEANTYPE(This)){
                case BOOLEANVAR:
                case ORDERCONST:
                        return;
                case PREDICATEOP:
-                       return computePredicatePolarityAndBooleanValue(boolean);
+                       return computePredicatePolarityAndBooleanValue((BooleanPredicate*)This);
                case LOGICOP:
-                       return computeLogicOpPolarityAndBooleanValue(boolean);
+                       return computeLogicOpPolarityAndBooleanValue((BooleanLogic*)This);
                default:
                        ASSERT(0);
        }
 }
 
-void computePredicatePolarityAndBooleanValue(Boolean* boolean){
-       ASSERT(GETBOOLEANTYPE(boolean) == PREDICATEOP);
-       BooleanPredicate* border= (BooleanPredicate*)boolean;
-       border->undefStatus->boolVal = GETBOOLEANVALUE(boolean);
-       border->undefStatus->polarity = GETBOOLEANPOLARITY(boolean);
-       computePolarityAndBooleanValue(border->undefStatus);
-}
-void computeLogicOpPolarityAndBooleanValue(Boolean* boolean){
-       ASSERT(GETBOOLEANTYPE(boolean) == LOGICOP);
-       computeLogicOpBooleanValue(boolean);
-       computeLogicOpPolarity(boolean);
-       uint size = getSizeArrayBoolean(& ((BooleanLogic*) boolean)->inputs);
-       for(uint i=0; i<size; i++){
-               computeLogicOpBooleanValue( getArrayBoolean(&((BooleanLogic*) boolean)->inputs, i) );
-       }
+void computePredicatePolarityAndBooleanValue(BooleanPredicate* This){
+       updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
+       computePolarityAndBooleanValue(This->undefStatus);
 }
-void computeLogicOpPolarity(Boolean* boolean){
-       BooleanLogic* This = (BooleanLogic*)boolean;
-       switch(This->op){
-               case L_AND:
-               case L_OR:{
-                       uint size = getSizeArrayBoolean(& This->inputs);
-                       for(uint i=0; i<size; i++){
-                               Boolean* tmp= getArrayBoolean(&This->inputs, i);
-                               tmp->polarity = computePolarity(tmp->polarity, boolean->polarity);
-                       }
-                       break;
-               }
-               case L_NOT:{
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==1);
-                       Boolean* tmp =getArrayBoolean(&This->inputs, 0);
-                       tmp->polarity = computePolarity(tmp->polarity, negatePolarity( boolean->polarity ) );
-                       break;
-               }case L_XOR:
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==2);
-                       getArrayBoolean(&This->inputs, 0)->polarity = P_BOTHTRUEFALSE;
-                       getArrayBoolean(&This->inputs, 1)->polarity = P_BOTHTRUEFALSE;
-                       break;
-               case L_IMPLIES:{
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==2);
-                       Boolean* tmp =getArrayBoolean(&This->inputs, 0);
-                       tmp->polarity = computePolarity(tmp->polarity, negatePolarity( boolean->polarity ));
-                       tmp = getArrayBoolean(&This->inputs, 1);  
-                       tmp->polarity= computePolarity(tmp->polarity, boolean->polarity) ;
-                       break;
-               }
-               default:
-                       ASSERT(0);
+
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic* This) {
+       computeLogicOpBooleanValue(This);
+       computeLogicOpPolarity(This);
+       uint size = getSizeArrayBoolean(&This->inputs);
+       for(uint i=0; i<size; i++) {
+               computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
        }
-       
 }
-void computeLogicOpBooleanValue(Boolean* boolean){
-       BooleanLogic* This = (BooleanLogic*)boolean;
-       switch(This->op){
-               case L_AND:
-               case L_OR:{
-                       uint size = getSizeArrayBoolean(& This->inputs);
-                       for(uint i=0; i<size; i++){
-                               Boolean* tmp= getArrayBoolean(&This->inputs, i);
-                               tmp->boolVal = computeBooleanValue(This->op, tmp->boolVal, boolean->boolVal);
-                       }
-                       return;
-               }
-               case L_XOR:
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==2);
-                       getArrayBoolean(&This->inputs, 0)->boolVal = BV_UNKNOWN;
-                       getArrayBoolean(&This->inputs, 1)->boolVal = BV_UNKNOWN;
-                       return;
-               case L_NOT:
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==1);
-                       Boolean* tmp =getArrayBoolean(&This->inputs, 0);
-                       tmp->boolVal = computeBooleanValue(This->op, tmp->boolVal,  boolean->boolVal  );
-                       return;
-               case L_IMPLIES:
-                       ASSERT( getSizeArrayBoolean(&This->inputs)==2);
-                       Boolean* p1= getArrayBoolean(&This->inputs, 0);
-                       Boolean* p2= getArrayBoolean(&This->inputs, 1);
-                       computeImplicationBooleanValue(p1, p2, boolean->boolVal);
-                       return;
+
+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);
        }
 }
 
-void computeImplicationBooleanValue(Boolean* first, Boolean* second, BooleanValue parent){
-       switch(parent){
+BooleanValue negateBooleanValue(BooleanValue This) {
+       switch(This){
+               case BV_UNDEFINED:
+               case BV_UNSAT:
+                       return This;
                case BV_MUSTBETRUE:
-               case BV_UNKNOWN:
-                       first->boolVal = BV_UNKNOWN;
-                       second->boolVal = BV_UNKNOWN;
+                       return BV_MUSTBEFALSE;
                case BV_MUSTBEFALSE:
-                       first->boolVal = BV_MUSTBETRUE;
-                       second->boolVal = BV_MUSTBEFALSE;
+                       return BV_MUSTBETRUE;
                default:
                        ASSERT(0);
        }
 }
 
-Polarity computePolarity(Polarity childPol, Polarity parentPol){
-       switch(childPol){
-               case P_UNDEFINED:
-                       return parentPol;
-               case P_TRUE: 
-               case P_FALSE:
-                       if(parentPol == childPol)
-                               return parentPol;
-                       else
-                               return P_BOTHTRUEFALSE;
-               case P_BOTHTRUEFALSE:
-                       return childPol;
-               default:
-                       ASSERT(0);
+void computeLogicOpPolarity(BooleanLogic* This) {
+       Polarity parentpolarity=GETBOOLEANPOLARITY(This);
+       switch(This->op){
+       case L_AND:
+       case L_OR:{
+               uint size = getSizeArrayBoolean(& This->inputs);
+               for(uint i=0; i<size; i++){
+                       Boolean* tmp= getArrayBoolean(&This->inputs, i);
+                       updatePolarity(tmp, parentpolarity);
+               }
+               break;
+       }
+       case L_NOT:{
+               Boolean* tmp =getArrayBoolean(&This->inputs, 0);
+               updatePolarity(tmp, negatePolarity(parentpolarity));
+               break;
+       }
+       case L_XOR: {
+               updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
+               updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
+               break;
+       }
+       case L_IMPLIES:{
+               Boolean* left = getArrayBoolean(&This->inputs, 0);
+               updatePolarity(left, negatePolarity( parentpolarity));
+               Boolean *right = getArrayBoolean(&This->inputs, 1);  
+               updatePolarity(right, parentpolarity);
+               break;
+       }
+       default:
+               ASSERT(0);
        }
-       exit(-1);
 }
 
-BooleanValue computeBooleanValue(LogicOp op, BooleanValue childVal, BooleanValue parentVal ){
-       switch(op){
-               case L_AND:
-                       if(childVal == BV_UNDEFINED && parentVal == BV_MUSTBETRUE){
-                               return parentVal;
-                       } else if(childVal != parentVal){
-                               return BV_UNKNOWN;
-                       } else
-                               return childVal;
-               case L_OR:
-                       if(childVal == BV_UNDEFINED && parentVal == BV_MUSTBEFALSE){
-                               return parentVal;
-                       } else if(childVal != parentVal){
-                               return BV_UNKNOWN;
-                       } else 
-                               return childVal;
-               case L_NOT:{
-                       BooleanValue newVal = negateBooleanValue(parentVal);
-                       if(childVal == BV_UNDEFINED){
-                               return newVal;
-                       } else if(childVal != newVal){
-                               return BV_UNKNOWN;
-                       } else 
-                               return childVal;
+void computeLogicOpBooleanValue(BooleanLogic* This) {
+       BooleanValue parentbv = GETBOOLEANVALUE(This);
+       switch(This->op){
+       case L_AND: {
+               if (parentbv==BV_MUSTBETRUE || parentbv==BV_UNSAT) {
+                       uint size = getSizeArrayBoolean(& This->inputs);
+                       for(uint i=0; i<size; i++) {
+                               updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+                       }
                }
-               default:
-                       ASSERT(0);
+               return;
+       }
+       case L_OR: {
+               if (parentbv==BV_MUSTBEFALSE || parentbv==BV_UNSAT) {
+                       uint size = getSizeArrayBoolean(& This->inputs);
+                       for(uint i=0; i<size; i++) {
+                               updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+                       }
+               }
+               return;
+       }
+       case L_NOT:
+               updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+               return;
+       case L_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);
+               }
+               return;
+       case L_XOR:
+               return;
+       default:
+               ASSERT(0);
        }
-       exit(-1);
-}
\ No newline at end of file
+}

diff --git a/src/Encoders/polarityassignment.h b/src/Encoders/polarityassignment.h
index 93595fddeb837db7f7ee885162d93ef3ba26a9a9..5acbd9ba117fb628727b359d453c25a88f2919f2 100644 (file)
--- a/src/Encoders/polarityassignment.h
+++ b/src/Encoders/polarityassignment.h
@@ -13,18 +13,15 @@
 #include "ops.h"
 #include "boolean.h"
 
-void assignPolarityAndBooleanValue(Boolean* boolean);
-void assignPolarityAndBooleanValue(Boolean* boolean);
-void assignPredicatePolarityAndBooleanValue(Boolean* boolean);
-void assignLogicOpPolarityAndBooleanValue(Boolean* boolean);
-void computeLogicOpPolarity(Boolean* boolean);
-void computeLogicOpBooleanValue(Boolean* boolean);
-void computeImplicationBooleanValue(Boolean* first, Boolean* second, BooleanValue parent);
+void computePolarities(CSolver* This);
+void updatePolarity(Boolean *This, Polarity polarity);
+void updateMustValue(Boolean *This, BooleanValue value);
 void computePolarityAndBooleanValue(Boolean* boolean);
-void computePredicatePolarityAndBooleanValue(Boolean* boolean);
-void computeLogicOpPolarityAndBooleanValue(Boolean* boolean);
-BooleanValue computeBooleanValue(LogicOp op, BooleanValue childVal, BooleanValue parentVal );
-Polarity computePolarity(Polarity childPol, Polarity parentPol);
-
+void computePredicatePolarityAndBooleanValue(BooleanPredicate* This);
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic* boolean);
+Polarity negatePolarity(Polarity This);
+BooleanValue negateBooleanValue(BooleanValue This);
+void computeLogicOpPolarity(BooleanLogic* boolean);
+void computeLogicOpBooleanValue(BooleanLogic* boolean);
 
 #endif /* POLARITYASSIGNMENT_H */