src/ASTAnalyses/polarityassignment.cc

   1 #include "polarityassignment.h"
   2 #include "csolver.h"
   3
   4 void computePolarities(CSolver *This) {
   5         SetIteratorBooleanEdge *iterator = This->getConstraints();
   6         while (iterator->hasNext()) {
   7                 BooleanEdge boolean = iterator->next();
   8                 Boolean *b = boolean.getBoolean();
   9                 bool isNegated = boolean.isNegated();
  10                 if (isNegated) {
  11                         updatePolarity(b, P_FALSE);
  12                         updateMustValue(b, BV_MUSTBEFALSE);
  13                 } else {
  14                         updatePolarity(b, P_TRUE);
  15                         updateMustValue(b, BV_MUSTBETRUE);
  16                 }
  17                 computePolarityAndBooleanValue(b);
  18         }
  19         delete iterator;
  20 }
  21
  22 void updatePolarity(Boolean *This, Polarity polarity) {
  23         This->polarity = (Polarity) (This->polarity | polarity);
  24 }
  25
  26 void updateMustValue(Boolean *This, BooleanValue value) {
  27         This->boolVal = (BooleanValue) (This->boolVal | value);
  28 }
  29
  30 void computePolarityAndBooleanValue(Boolean *This) {
  31         switch (This->type) {
  32         case BOOLEANVAR:
  33         case ORDERCONST:
  34                 return;
  35         case PREDICATEOP:
  36                 return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
  37         case LOGICOP:
  38                 return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
  39         default:
  40                 ASSERT(0);
  41         }
  42 }
  43
  44 void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
  45         if (This->undefStatus) {
  46                 updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
  47                 computePolarityAndBooleanValue(This->undefStatus.getBoolean());
  48         }
  49 }
  50
  51 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
  52         computeLogicOpBooleanValue(This);
  53         computeLogicOpPolarity(This);
  54         uint size = This->inputs.getSize();
  55         for (uint i = 0; i < size; i++) {
  56                 computePolarityAndBooleanValue(This->inputs.get(i).getBoolean());
  57         }
  58 }
  59
  60 Polarity negatePolarity(Polarity This) {
  61         switch (This) {
  62         case P_UNDEFINED:
  63         case P_BOTHTRUEFALSE:
  64                 return This;
  65         case P_TRUE:
  66                 return P_FALSE;
  67         case P_FALSE:
  68                 return P_TRUE;
  69         default:
  70                 ASSERT(0);
  71         }
  72 }
  73
  74 BooleanValue negateBooleanValue(BooleanValue This) {
  75         switch (This) {
  76         case BV_UNDEFINED:
  77         case BV_UNSAT:
  78                 return This;
  79         case BV_MUSTBETRUE:
  80                 return BV_MUSTBEFALSE;
  81         case BV_MUSTBEFALSE:
  82                 return BV_MUSTBETRUE;
  83         default:
  84                 ASSERT(0);
  85         }
  86 }
  87
  88 void computeLogicOpPolarity(BooleanLogic *This) {
  89         Polarity parentpolarity = This->polarity;
  90         switch (This->op) {
  91         case SATC_AND: {
  92                 uint size = This->inputs.getSize();
  93                 for (uint i = 0; i < size; i++) {
  94                         BooleanEdge tmp = This->inputs.get(i);
  95                         Boolean *btmp = tmp.getBoolean();
  96                         updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
  97                 }
  98                 break;
  99         }
 100         case SATC_IFF: {
 101                 updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
 102                 updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
 103                 break;
 104         }
 105         default:
 106                 ASSERT(0);
 107         }
 108 }
 109
 110 void computeLogicOpBooleanValue(BooleanLogic *This) {
 111         BooleanValue parentbv = This->boolVal;
 112         switch (This->op) {
 113         case SATC_AND: {
 114                 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
 115                         uint size = This->inputs.getSize();
 116                         for (uint i = 0; i < size; i++) {
 117                                 BooleanEdge be=This->inputs.get(i);
 118                                 updateMustValue(be.getBoolean(), be.isNegated()?negateBooleanValue(parentbv):parentbv);
 119                         }
 120                 }
 121                 return;
 122         }
 123         case SATC_IFF:
 124                 return;
 125         default:
 126                 ASSERT(0);
 127         }
 128 }