src/ASTAnalyses/Polarity/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                 computePolarity(b, isNegated ? P_FALSE : P_TRUE);
  11         }
  12         delete iterator;
  13 }
  14
  15 void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
  16         Boolean *bdst = dst.getBoolean();
  17         Boolean *bsrc = src.getBoolean();
  18         bool isNegated = dst.isNegated() ^ src.isNegated();
  19         Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
  20         updatePolarity(bdst, p);
  21 }
  22
  23 void updateEdgePolarity(BooleanEdge dst, Polarity p) {
  24         Boolean *bdst = dst.getBoolean();
  25         bool isNegated = dst.isNegated();
  26         if (isNegated)
  27                 p = negatePolarity(p);
  28         updatePolarity(bdst, p);
  29 }
  30
  31 bool updatePolarity(Boolean *This, Polarity polarity) {
  32         Polarity oldpolarity = This->polarity;
  33         Polarity newpolarity = (Polarity) (This->polarity | polarity);
  34         This->polarity = newpolarity;
  35         return newpolarity != oldpolarity;
  36 }
  37
  38 void updateMustValue(Boolean *This, BooleanValue value) {
  39         This->boolVal = (BooleanValue) (This->boolVal | value);
  40 }
  41
  42 void computePolarity(Boolean *This, Polarity polarity) {
  43         if (updatePolarity(This, polarity)) {
  44                 switch (This->type) {
  45                 case BOOLEANVAR:
  46                 case ORDERCONST:
  47                 case BOOLCONST:
  48                         return;
  49                 case PREDICATEOP:
  50                         return computePredicatePolarity((BooleanPredicate *)This);
  51                 case LOGICOP:
  52                         return computeLogicOpPolarity((BooleanLogic *)This);
  53                 default:
  54                         ASSERT(0);
  55                 }
  56         }
  57 }
  58
  59 void computePredicatePolarity(BooleanPredicate *This) {
  60         if (This->undefStatus) {
  61                 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
  62         }
  63         for (uint i = 0; i < This->inputs.getSize(); i++) {
  64                 Element *e = This->inputs.get(i);
  65                 computeElement(e);
  66         }
  67 }
  68
  69 void computeElement(Element *e) {
  70         if (e->type == ELEMFUNCRETURN) {
  71                 ElementFunction *ef = (ElementFunction *) e;
  72
  73                 if (ef->overflowstatus) {
  74                         computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
  75                 }
  76
  77                 for (uint i = 0; i < ef->inputs.getSize(); i++) {
  78                         Element *echild = ef->inputs.get(i);
  79                         computeElement(echild);
  80                 }
  81         }
  82 }
  83
  84 void computeLogicOpPolarity(BooleanLogic *This) {
  85         Polarity child = computeLogicOpPolarityChildren(This);
  86         uint size = This->inputs.getSize();
  87         for (uint i = 0; i < size; i++) {
  88                 BooleanEdge b = This->inputs.get(i);
  89                 computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
  90         }
  91 }
  92
  93 BooleanValue negateBooleanValue(BooleanValue This) {
  94         switch (This) {
  95         case BV_UNDEFINED:
  96         case BV_UNSAT:
  97                 return This;
  98         case BV_MUSTBETRUE:
  99                 return BV_MUSTBEFALSE;
 100         case BV_MUSTBEFALSE:
 101                 return BV_MUSTBETRUE;
 102         default:
 103                 ASSERT(0);
 104         }
 105 }
 106
 107 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
 108         switch (This->op) {
 109         case SATC_AND: {
 110                 return This->polarity;
 111         }
 112         case SATC_IFF: {
 113                 return P_BOTHTRUEFALSE;
 114         }
 115         default:
 116                 ASSERT(0);
 117         }
 118 }
 119
 120 Polarity negatePolarity(Polarity This) {
 121         switch (This) {
 122         case P_UNDEFINED:
 123         case P_BOTHTRUEFALSE:
 124                 return This;
 125         case P_TRUE:
 126                 return P_FALSE;
 127         case P_FALSE:
 128                 return P_TRUE;
 129         default:
 130                 ASSERT(0);
 131         }
 132 }