Assigning Polarity and BooleanValue to All the Boolean Constraints

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index e4e9ddd0ac729d68b1d83482974ca71c4174e875..09ec2ae817de133940927287c7e68d65fe0427f7 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -7,6 +7,8 @@
 Boolean* allocBooleanVar(VarType t) {
        BooleanVar* This=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
        GETBOOLEANTYPE(This)=BOOLEANVAR;
+       GETBOOLEANVALUE(This) = BV_UNDEFINED;
+       GETBOOLEANPOLARITY(This) = P_UNDEFINED;
        This->vtype=t;
        This->var=E_NULL;
        initDefVectorBoolean(GETBOOLEANPARENTS(This));
@@ -16,6 +18,8 @@ Boolean* allocBooleanVar(VarType t) {
 Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        BooleanOrder* This=(BooleanOrder *) ourmalloc(sizeof (BooleanOrder));
        GETBOOLEANTYPE(This)=ORDERCONST;
+       GETBOOLEANVALUE(This) = BV_UNDEFINED;
+       GETBOOLEANPOLARITY(This) = P_UNDEFINED;
        This->order=order;
        This->first=first;
        This->second=second;
@@ -27,6 +31,8 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
        BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
        GETBOOLEANTYPE(This)= PREDICATEOP;
+       GETBOOLEANVALUE(This) = BV_UNDEFINED;
+       GETBOOLEANPOLARITY(This) = P_UNDEFINED;
        This->predicate=predicate;
        initArrayInitElement(&This->inputs, inputs, numInputs);
        initDefVectorBoolean(GETBOOLEANPARENTS(This));
@@ -42,6 +48,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
        BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
        GETBOOLEANTYPE(This) = LOGICOP;
+       GETBOOLEANVALUE(This) = BV_UNDEFINED;
+       GETBOOLEANPOLARITY(This) = P_UNDEFINED;
        This->op = op;
        initDefVectorBoolean(GETBOOLEANPARENTS(This));
        initArrayInitBoolean(&This->inputs, array, asize);
@@ -68,3 +76,33 @@ 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 3d3a90639b8b7596c2849fdc749e233ae6ebecb8..b24fa3f83e10d9cf093b6478bb515e7710507317 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -14,9 +14,13 @@
 
 #define GETBOOLEANTYPE(o) GETASTNODETYPE(o)
 #define GETBOOLEANPARENTS(o) (&((Boolean *)(o))->parents)
+#define GETBOOLEANPOLARITY(b) (((Boolean*)b)->polarity)
+#define GETBOOLEANVALUE(b) (((Boolean*)b)->boolVal)
 
 struct Boolean {
        ASTNode base;
+       Polarity polarity;
+       BooleanValue boolVal;
        VectorBoolean parents;
 };
 
@@ -52,7 +56,8 @@ 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 32febff340161729dd67fb0e69312038d02923ab..9e8113d685ce48bd0e3f8dab0b7e38b1823d3c4b 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -38,4 +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};
+typedef enum Polarity Polarity;
+
+enum BooleanValue {BV_UNDEFINED, BV_MUSTBETRUE, BV_MUSTBEFALSE, BV_UNKNOWN};
+typedef enum BooleanValue BooleanValue;
+
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 3bb927cf722abd076bfb1f0b71260ca35baa7fcf..3baada358e4ba904efe62e36acb9a911463a0376 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -11,11 +11,14 @@
 #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++) {
-               naiveEncodingConstraint(getVectorBoolean(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
new file mode 100644 (file)
index 0000000..840df1b
--- /dev/null
+++ b/src/Encoders/polarityassignment.c
@@ -0,0 +1,168 @@
+#include "polarityassignment.h"
+
+void assignPolarityAndBooleanValue(Boolean* boolean){
+       GETBOOLEANPOLARITY(boolean) = P_TRUE;
+       GETBOOLEANVALUE(boolean) = BV_MUSTBETRUE;
+       computePolarityAndBooleanValue(boolean);
+}
+
+void computePolarityAndBooleanValue(Boolean* boolean){
+       switch( GETBOOLEANTYPE(boolean)){
+               case BOOLEANVAR:
+               case ORDERCONST:
+                       return;
+               case PREDICATEOP:
+                       return computePredicatePolarityAndBooleanValue(boolean);
+               case LOGICOP:
+                       return computeLogicOpPolarityAndBooleanValue(boolean);
+               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 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 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;
+               default:
+                       ASSERT(0);
+       }
+}
+
+void computeImplicationBooleanValue(Boolean* first, Boolean* second, BooleanValue parent){
+       switch(parent){
+               case BV_MUSTBETRUE:
+               case BV_UNKNOWN:
+                       first->boolVal = BV_UNKNOWN;
+                       second->boolVal = BV_UNKNOWN;
+               case BV_MUSTBEFALSE:
+                       first->boolVal = BV_MUSTBETRUE;
+                       second->boolVal = BV_MUSTBEFALSE;
+               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);
+       }
+       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;
+               }
+               default:
+                       ASSERT(0);
+       }
+       exit(-1);
+}
\ No newline at end of file

diff --git a/src/Encoders/polarityassignment.h b/src/Encoders/polarityassignment.h
new file mode 100644 (file)
index 0000000..93595fd
--- /dev/null
+++ b/src/Encoders/polarityassignment.h
@@ -0,0 +1,30 @@
+/* 
+ * File:   polarityassignment.h
+ * Author: hamed
+ *
+ * Created on August 6, 2017, 12:18 PM
+ */
+
+#ifndef POLARITYASSIGNMENT_H
+#define POLARITYASSIGNMENT_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "common.h"
+#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 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);
+
+
+#endif /* POLARITYASSIGNMENT_H */