src/Encoders/polarityassignment.c

   1 #include "polarityassignment.h"
   2 #include "csolver.h"
   3
   4 void computePolarities(CSolver* This) {
   5         for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
   6                 Boolean* boolean = getVectorBoolean(This->constraints, i);
   7                 updatePolarity(boolean, P_TRUE);
   8                 updateMustValue(boolean, BV_MUSTBETRUE);
   9                 computePolarityAndBooleanValue(boolean);
  10         }
  11 }
  12
  13 void updatePolarity(Boolean *This, Polarity polarity) {
  14         This->polarity |= polarity;
  15 }
  16
  17 void updateMustValue(Boolean *This, BooleanValue value) {
  18         This->boolVal |= value;
  19 }
  20
  21 void computePolarityAndBooleanValue(Boolean* This) {
  22         switch(GETBOOLEANTYPE(This)){
  23                 case BOOLEANVAR:
  24                 case ORDERCONST:
  25                         return;
  26                 case PREDICATEOP:
  27                         return computePredicatePolarityAndBooleanValue((BooleanPredicate*)This);
  28                 case LOGICOP:
  29                         return computeLogicOpPolarityAndBooleanValue((BooleanLogic*)This);
  30                 default:
  31                         ASSERT(0);
  32         }
  33 }
  34
  35 void computePredicatePolarityAndBooleanValue(BooleanPredicate* This){
  36         updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
  37         computePolarityAndBooleanValue(This->undefStatus);
  38 }
  39
  40 void computeLogicOpPolarityAndBooleanValue(BooleanLogic* This) {
  41         computeLogicOpBooleanValue(This);
  42         computeLogicOpPolarity(This);
  43         uint size = getSizeArrayBoolean(&This->inputs);
  44         for(uint i=0; i<size; i++) {
  45                 computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
  46         }
  47 }
  48
  49 Polarity negatePolarity(Polarity This) {
  50         switch(This){
  51                 case P_UNDEFINED:
  52                 case P_BOTHTRUEFALSE:
  53                         return This;
  54                 case P_TRUE:
  55                         return P_FALSE;
  56                 case P_FALSE:
  57                         return P_TRUE;
  58                 default:
  59                         ASSERT(0);
  60         }
  61 }
  62
  63 BooleanValue negateBooleanValue(BooleanValue This) {
  64         switch(This){
  65                 case BV_UNDEFINED:
  66                 case BV_UNSAT:
  67                         return This;
  68                 case BV_MUSTBETRUE:
  69                         return BV_MUSTBEFALSE;
  70                 case BV_MUSTBEFALSE:
  71                         return BV_MUSTBETRUE;
  72                 default:
  73                         ASSERT(0);
  74         }
  75 }
  76
  77 void computeLogicOpPolarity(BooleanLogic* This) {
  78         Polarity parentpolarity=GETBOOLEANPOLARITY(This);
  79         switch(This->op){
  80         case L_AND:
  81         case L_OR:{
  82                 uint size = getSizeArrayBoolean(& This->inputs);
  83                 for(uint i=0; i<size; i++){
  84                         Boolean* tmp= getArrayBoolean(&This->inputs, i);
  85                         updatePolarity(tmp, parentpolarity);
  86                 }
  87                 break;
  88         }
  89         case L_NOT:{
  90                 Boolean* tmp =getArrayBoolean(&This->inputs, 0);
  91                 updatePolarity(tmp, negatePolarity(parentpolarity));
  92                 break;
  93         }
  94         case L_XOR: {
  95                 updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
  96                 updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
  97                 break;
  98         }
  99         case L_IMPLIES:{
 100                 Boolean* left = getArrayBoolean(&This->inputs, 0);
 101                 updatePolarity(left, negatePolarity( parentpolarity));
 102                 Boolean *right = getArrayBoolean(&This->inputs, 1);
 103                 updatePolarity(right, parentpolarity);
 104                 break;
 105         }
 106         default:
 107                 ASSERT(0);
 108         }
 109 }
 110
 111 void computeLogicOpBooleanValue(BooleanLogic* This) {
 112         BooleanValue parentbv = GETBOOLEANVALUE(This);
 113         switch(This->op){
 114         case L_AND: {
 115                 if (parentbv==BV_MUSTBETRUE || parentbv==BV_UNSAT) {
 116                         uint size = getSizeArrayBoolean(& This->inputs);
 117                         for(uint i=0; i<size; i++) {
 118                                 updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
 119                         }
 120                 }
 121                 return;
 122         }
 123         case L_OR: {
 124                 if (parentbv==BV_MUSTBEFALSE || parentbv==BV_UNSAT) {
 125                         uint size = getSizeArrayBoolean(& This->inputs);
 126                         for(uint i=0; i<size; i++) {
 127                                 updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
 128                         }
 129                 }
 130                 return;
 131         }
 132         case L_NOT:
 133                 updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
 134                 return;
 135         case L_IMPLIES:
 136                 //implies is really an or with the first term negated
 137                 if (parentbv==BV_MUSTBEFALSE || parentbv==BV_UNSAT) {
 138                         uint size = getSizeArrayBoolean(& This->inputs);
 139                         updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
 140                         updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
 141                 }
 142                 return;
 143         case L_XOR:
 144                 return;
 145         default:
 146                 ASSERT(0);
 147         }
 148 }