From bd3c5e0014fd56964171bdc3f6bb774b242bd4a0 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 8 Aug 2017 21:53:32 -0700 Subject: [PATCH] Clean up polarity pass --- src/AST/boolean.c | 30 ---- src/AST/boolean.h | 2 - src/AST/ops.h | 4 +- src/Encoders/naiveencoder.c | 2 - src/Encoders/polarityassignment.c | 248 ++++++++++++++---------------- src/Encoders/polarityassignment.h | 21 ++- 6 files changed, 125 insertions(+), 182 deletions(-) diff --git a/src/AST/boolean.c b/src/AST/boolean.c index 09ec2ae..591bfe6 100644 --- 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 b24fa3f..2a80d39 100644 --- 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 9e8113d..c9de82d 100644 --- 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 3baada3..bc64cc4 100644 --- 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 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 840df1b..0ad5f88 100644 --- 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; iinputs, 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; 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 computeLogicOpPolarityAndBooleanValue(BooleanLogic* This) { + computeLogicOpBooleanValue(This); + computeLogicOpPolarity(This); + uint size = getSizeArrayBoolean(&This->inputs); + for(uint i=0; iinputs, 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; 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; + +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; iinputs, 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; iinputs, 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; iinputs, 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 93595fd..5acbd9b 100644 --- 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 */ -- 2.34.1