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                 } else {
  13                         updatePolarity(b, P_TRUE);
  14                 }
  15                 computePolarity(b);
  16         }
  17         delete iterator;
  18 }
  19
  20 void updatePolarity(Boolean *This, Polarity polarity) {
  21         This->polarity = (Polarity) (This->polarity | polarity);
  22 }
  23
  24 void updateMustValue(Boolean *This, BooleanValue value) {
  25         This->boolVal = (BooleanValue) (This->boolVal | value);
  26 }
  27
  28 void computePolarity(Boolean *This) {
  29         switch (This->type) {
  30         case BOOLEANVAR:
  31         case ORDERCONST:
  32                 return;
  33         case PREDICATEOP:
  34                 return computePredicatePolarity((BooleanPredicate *)This);
  35         case LOGICOP:
  36                 return computeLogicOpPolarity((BooleanLogic *)This);
  37         default:
  38                 ASSERT(0);
  39         }
  40 }
  41
  42 void computePredicatePolarity(BooleanPredicate *This) {
  43         if (This->undefStatus) {
  44                 updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
  45                 computePolarity(This->undefStatus.getBoolean());
  46         }
  47 }
  48
  49 void computeLogicOpPolarity(BooleanLogic *This) {
  50         computeLogicOpPolarityChildren(This);
  51         uint size = This->inputs.getSize();
  52         for (uint i = 0; i < size; i++) {
  53                 computePolarity(This->inputs.get(i).getBoolean());
  54         }
  55 }
  56
  57 Polarity negatePolarity(Polarity This) {
  58         switch (This) {
  59         case P_UNDEFINED:
  60         case P_BOTHTRUEFALSE:
  61                 return This;
  62         case P_TRUE:
  63                 return P_FALSE;
  64         case P_FALSE:
  65                 return P_TRUE;
  66         default:
  67                 ASSERT(0);
  68         }
  69 }
  70
  71 BooleanValue negateBooleanValue(BooleanValue This) {
  72         switch (This) {
  73         case BV_UNDEFINED:
  74         case BV_UNSAT:
  75                 return This;
  76         case BV_MUSTBETRUE:
  77                 return BV_MUSTBEFALSE;
  78         case BV_MUSTBEFALSE:
  79                 return BV_MUSTBETRUE;
  80         default:
  81                 ASSERT(0);
  82         }
  83 }
  84
  85 void computeLogicOpPolarityChildren(BooleanLogic *This) {
  86         Polarity parentpolarity = This->polarity;
  87         switch (This->op) {
  88         case SATC_AND: {
  89                 uint size = This->inputs.getSize();
  90                 for (uint i = 0; i < size; i++) {
  91                         BooleanEdge tmp = This->inputs.get(i);
  92                         Boolean *btmp = tmp.getBoolean();
  93                         updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
  94                 }
  95                 break;
  96         }
  97         case SATC_IFF: {
  98                 updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
  99                 updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
 100                 break;
 101         }
 102         default:
 103                 ASSERT(0);
 104         }
 105 }