src/ASTAnalyses/Polarity/polarityassignment.cc

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