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                 uint size = This->inputs.getSize();
  86                 for (uint i = 0; i < size; i++) {
  87                         Boolean *tmp = This->inputs.get(i);
  88                         updatePolarity(tmp, parentpolarity);
  89                 }
  90                 break;
  91         }
  92         case SATC_NOT: {
  93                 Boolean *tmp = This->inputs.get(0);
  94                 updatePolarity(tmp, negatePolarity(parentpolarity));
  95                 break;
  96         }
  97         case SATC_IFF: {
  98                 updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
  99                 updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
 100                 break;
 101         }
 102         default:
 103                 ASSERT(0);
 104         }
 105 }
 106
 107 void computeLogicOpBooleanValue(BooleanLogic *This) {
 108         BooleanValue parentbv = This->boolVal;
 109         switch (This->op) {
 110         case SATC_AND: {
 111                 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
 112                         uint size = This->inputs.getSize();
 113                         for (uint i = 0; i < size; i++) {
 114                                 updateMustValue(This->inputs.get(i), parentbv);
 115                         }
 116                 }
 117                 return;
 118         }
 119         case SATC_NOT:
 120                 updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 121                 return;
 122         case SATC_IFF:
 123                 return;
 124         default:
 125                 ASSERT(0);
 126         }
 127 }