src/ASTAnalyses/polarityassignment.cc

   1 #include "polarityassignment.h"
   2 #include "csolver.h"
   3
   4 void computePolarities(CSolver *This) {
   5         SetIteratorBoolean *iterator = This->getConstraints();
   6         while (iterator->hasNext()) {
   7                 Boolean *boolean = iterator->next();
   8                 updatePolarity(boolean, P_TRUE);
   9                 updateMustValue(boolean, BV_MUSTBETRUE);
  10                 computePolarityAndBooleanValue(boolean);
  11         }
  12         delete iterator;
  13 }
  14
  15 void updatePolarity(Boolean *This, Polarity polarity) {
  16         This->polarity = (Polarity) (This->polarity | polarity);
  17 }
  18
  19 void updateMustValue(Boolean *This, BooleanValue value) {
  20         This->boolVal = (BooleanValue) (This->boolVal | value);
  21 }
  22
  23 void computePolarityAndBooleanValue(Boolean *This) {
  24         switch (This->type) {
  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         if (This->undefStatus != NULL) {
  39                 updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
  40                 computePolarityAndBooleanValue(This->undefStatus);
  41         }
  42 }
  43
  44 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
  45         computeLogicOpBooleanValue(This);
  46         computeLogicOpPolarity(This);
  47         uint size = This->inputs.getSize();
  48         for (uint i = 0; i < size; i++) {
  49                 computePolarityAndBooleanValue(This->inputs.get(i));
  50         }
  51 }
  52
  53 Polarity negatePolarity(Polarity This) {
  54         switch (This) {
  55         case P_UNDEFINED:
  56         case P_BOTHTRUEFALSE:
  57                 return This;
  58         case P_TRUE:
  59                 return P_FALSE;
  60         case P_FALSE:
  61                 return P_TRUE;
  62         default:
  63                 ASSERT(0);
  64         }
  65 }
  66
  67 BooleanValue negateBooleanValue(BooleanValue This) {
  68         switch (This) {
  69         case BV_UNDEFINED:
  70         case BV_UNSAT:
  71                 return This;
  72         case BV_MUSTBETRUE:
  73                 return BV_MUSTBEFALSE;
  74         case BV_MUSTBEFALSE:
  75                 return BV_MUSTBETRUE;
  76         default:
  77                 ASSERT(0);
  78         }
  79 }
  80
  81 void computeLogicOpPolarity(BooleanLogic *This) {
  82         Polarity parentpolarity = This->polarity;
  83         switch (This->op) {
  84         case SATC_AND:
  85         case SATC_OR: {
  86                 uint size = This->inputs.getSize();
  87                 for (uint i = 0; i < size; i++) {
  88                         Boolean *tmp = This->inputs.get(i);
  89                         updatePolarity(tmp, parentpolarity);
  90                 }
  91                 break;
  92         }
  93         case SATC_NOT: {
  94                 Boolean *tmp = This->inputs.get(0);
  95                 updatePolarity(tmp, negatePolarity(parentpolarity));
  96                 break;
  97         }
  98         case SATC_IFF:
  99         case SATC_XOR: {
 100                 updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
 101                 updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
 102                 break;
 103         }
 104         case SATC_IMPLIES: {
 105                 Boolean *left = This->inputs.get(0);
 106                 updatePolarity(left, negatePolarity( parentpolarity));
 107                 Boolean *right = This->inputs.get(1);
 108                 updatePolarity(right, parentpolarity);
 109                 break;
 110         }
 111         default:
 112                 ASSERT(0);
 113         }
 114 }
 115
 116 void computeLogicOpBooleanValue(BooleanLogic *This) {
 117         BooleanValue parentbv = This->boolVal;
 118         switch (This->op) {
 119         case SATC_AND: {
 120                 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
 121                         uint size = This->inputs.getSize();
 122                         for (uint i = 0; i < size; i++) {
 123                                 updateMustValue(This->inputs.get(i), parentbv);
 124                         }
 125                 }
 126                 return;
 127         }
 128         case SATC_OR: {
 129                 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
 130                         uint size = This->inputs.getSize();
 131                         for (uint i = 0; i < size; i++) {
 132                                 updateMustValue(This->inputs.get(i), parentbv);
 133                         }
 134                 }
 135                 return;
 136         }
 137         case SATC_NOT:
 138                 updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 139                 return;
 140         case SATC_IMPLIES:
 141                 //implies is really an or with the first term negated
 142                 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
 143                         uint size = This->inputs.getSize();
 144                         updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 145                         updateMustValue(This->inputs.get(1), parentbv);
 146                 }
 147                 return;
 148         case SATC_IFF:
 149         case SATC_XOR:
 150                 return;
 151         default:
 152                 ASSERT(0);
 153         }
 154 }