src/AST/rewriter.cc

   1 #include "rewriter.h"
   2 #include "boolean.h"
   3 #include "csolver.h"
   4 #include "polarityassignment.h"
   5
   6 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
   7         if (constraints.contains(bexpr.negate())) {
   8                 constraints.remove(bexpr.negate());
   9                 setUnSAT();
  10         }
  11         if (constraints.contains(bexpr)) {
  12                 constraints.remove(bexpr);
  13         }
  14
  15         replaceBooleanWithTrueNoRemove(bexpr);
  16 }
  17
  18 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
  19         updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
  20
  21         uint size = bexpr->parents.getSize();
  22         for (uint i = 0; i < size; i++) {
  23                 Boolean *parent = bexpr->parents.get(i);
  24                 ASSERT(parent->type == LOGICOP);
  25                 BooleanLogic *logicop = (BooleanLogic *) parent;
  26                 switch (logicop->op) {
  27                 case SATC_AND:
  28                         handleANDTrue(logicop, bexpr);
  29                         break;
  30                 case SATC_IFF:
  31                         handleIFFTrue(logicop, bexpr);
  32                         break;
  33                 case SATC_NOT:
  34                 case SATC_OR:
  35                 case SATC_XOR:
  36                 case SATC_IMPLIES:
  37                         ASSERT(0);
  38                 }
  39         }
  40 }
  41
  42 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
  43         //Canonicalize
  44         if (oldb.isNegated()) {
  45                 oldb=oldb.negate();
  46                 newb=newb.negate();
  47         }
  48         if (constraints.contains(oldb)) {
  49                 constraints.remove(oldb);
  50                 constraints.add(newb);
  51         }
  52         if (constraints.contains(oldb.negate())) {
  53                 constraints.remove(oldb.negate());
  54                 constraints.add(newb.negate());
  55         }
  56
  57         BooleanEdge oldbnegated = oldb.negate();
  58         uint size = oldb->parents.getSize();
  59         for (uint i = 0; i < size; i++) {
  60                 Boolean *parent = oldb->parents.get(i);
  61                 BooleanLogic *logicop = (BooleanLogic *) parent;
  62
  63                 uint parentsize = logicop->inputs.getSize();
  64
  65                 for (uint j = 0; j < parentsize; j++) {
  66                         BooleanEdge b = logicop->inputs.get(i);
  67                         if (b == oldb) {
  68                                 logicop->inputs.set(i, newb);
  69                                 newb->parents.push(parent);
  70                         } else if (b == oldbnegated) {
  71                                 logicop->inputs.set(i, newb.negate());
  72                                 newb->parents.push(parent);
  73                         }
  74                 }
  75         }
  76 }
  77
  78 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
  79         uint size = bexpr->inputs.getSize();
  80         BooleanEdge b0 = bexpr->inputs.get(0);
  81         BooleanEdge b1 = bexpr->inputs.get(1);
  82         BooleanEdge childnegate = child.negate();
  83         bexpr->replaced = true;
  84         if (b0 == child) {
  85                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
  86         } else if (b0 == childnegate) {
  87                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
  88         } else if (b1 == child) {
  89                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
  90         } else if (b1 == childnegate) {
  91                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
  92         } else
  93                 ASSERT(0);
  94 }
  95
  96 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
  97         BooleanEdge childNegate=child.negate();
  98
  99         boolMap.remove(bexpr);
 100
 101         for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
 102                 BooleanEdge b = bexpr->inputs.get(i);
 103
 104                 if (b == child) {
 105                         bexpr->inputs.remove(i);
 106                         i--;
 107                 } else if (b == childNegate) {
 108                         replaceBooleanWithFalse(bexpr);
 109                         return;
 110                 }
 111         }
 112
 113         uint size=bexpr->inputs.getSize();
 114         if (size == 0) {
 115                 bexpr->replaced = true;
 116                 replaceBooleanWithTrue(bexpr);
 117         } else if (size == 1) {
 118                 bexpr->replaced = true;
 119                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
 120         } else {
 121                 //Won't build any of these in future cases...
 122                 boolMap.put(bexpr, bexpr);
 123         }
 124 }
 125
 126 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 127         replaceBooleanWithTrue(bexpr.negate());
 128 }
 129
 130 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
 131         bool isNegated=bexpr.isNegated();
 132         BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
 133         BooleanEdge result;
 134         if (b->op == SATC_IFF) {
 135                 if (isTrue(b->inputs.get(0))) {
 136                         result = b->inputs.get(1);
 137                 } else if (isFalse(b->inputs.get(0))) {
 138                         result = b->inputs.get(1).negate();
 139                 } else if (isTrue(b->inputs.get(1))) {
 140                         result = b->inputs.get(0);
 141                 } else if (isFalse(b->inputs.get(1))) {
 142                         result = b->inputs.get(0).negate();
 143                 } else ASSERT(0);
 144         } else if (b->op==SATC_AND) {
 145                 uint size = b->inputs.getSize();
 146                 if (size == 0)
 147                         result = boolTrue;
 148                 else if (size == 1)
 149                         result = b->inputs.get(0);
 150                 else ASSERT(0);
 151         }
 152         return isNegated ? result.negate() : result;
 153 }