From 2aea7b577106ca44a77ff23a9d2a1c597e3bd58f Mon Sep 17 00:00:00 2001 From: Hamed Date: Sun, 6 Aug 2017 20:05:49 -0700 Subject: [PATCH] Assigning Polarity and BooleanValue to All the Boolean Constraints --- src/AST/boolean.c | 38 +++++++ src/AST/boolean.h | 7 +- src/AST/ops.h | 6 ++ src/Encoders/naiveencoder.c | 5 +- src/Encoders/polarityassignment.c | 168 ++++++++++++++++++++++++++++++ src/Encoders/polarityassignment.h | 30 ++++++ 6 files changed, 252 insertions(+), 2 deletions(-) create mode 100644 src/Encoders/polarityassignment.c create mode 100644 src/Encoders/polarityassignment.h diff --git a/src/AST/boolean.c b/src/AST/boolean.c index e4e9ddd..09ec2ae 100644 --- 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 3d3a906..b24fa3f 100644 --- 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 32febff..9e8113d 100644 --- 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 3bb927c..3baada3 100644 --- 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 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 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; iinputs, 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; iinputs, 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; iinputs, 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 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 */ -- 2.34.1