src/Encoders/polarityassignment.c

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