src/ASTAnalyses/polarityassignment.cc

   1 #include "polarityassignment.h"
   2 #include "csolver.h"
   3
   4 void computePolarities(CSolver *This) {
   5         HSIteratorBoolean *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 L_AND:
  85         case L_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 L_NOT: {
  94                 Boolean *tmp = This->inputs.get(0);
  95                 updatePolarity(tmp, negatePolarity(parentpolarity));
  96                 break;
  97         }
  98         case L_XOR: {
  99                 updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
 100                 updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
 101                 break;
 102         }
 103         case L_IMPLIES: {
 104                 Boolean *left = This->inputs.get(0);
 105                 updatePolarity(left, negatePolarity( parentpolarity));
 106                 Boolean *right = This->inputs.get(1);
 107                 updatePolarity(right, parentpolarity);
 108                 break;
 109         }
 110         default:
 111                 ASSERT(0);
 112         }
 113 }
 114
 115 void computeLogicOpBooleanValue(BooleanLogic *This) {
 116         BooleanValue parentbv = This->boolVal;
 117         switch (This->op) {
 118         case L_AND: {
 119                 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
 120                         uint size = This->inputs.getSize();
 121                         for (uint i = 0; i < size; i++) {
 122                                 updateMustValue(This->inputs.get(i), parentbv);
 123                         }
 124                 }
 125                 return;
 126         }
 127         case L_OR: {
 128                 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
 129                         uint size = This->inputs.getSize();
 130                         for (uint i = 0; i < size; i++) {
 131                                 updateMustValue(This->inputs.get(i), parentbv);
 132                         }
 133                 }
 134                 return;
 135         }
 136         case L_NOT:
 137                 updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 138                 return;
 139         case L_IMPLIES:
 140                 //implies is really an or with the first term negated
 141                 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
 142                         uint size = This->inputs.getSize();
 143                         updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 144                         updateMustValue(This->inputs.get(1), parentbv);
 145                 }
 146                 return;
 147         case L_XOR:
 148                 return;
 149         default:
 150                 ASSERT(0);
 151         }
 152 }