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                 boolMap.remove(parent); //could change parent's hash
  63
  64                 uint parentsize = logicop->inputs.getSize();
  65                 for (uint j = 0; j < parentsize; j++) {
  66                         BooleanEdge b = logicop->inputs.get(j);
  67                         if (b == oldb) {
  68                                 logicop->inputs.set(j, newb);
  69                                 newb->parents.push(parent);
  70                         } else if (b == oldbnegated) {
  71                                 logicop->inputs.set(j, newb.negate());
  72                                 newb->parents.push(parent);
  73                         }
  74                 }
  75                 boolMap.put(parent, parent);
  76         }
  77 }
  78
  79 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
  80         uint size = bexpr->inputs.getSize();
  81         BooleanEdge b0 = bexpr->inputs.get(0);
  82         BooleanEdge b1 = bexpr->inputs.get(1);
  83         BooleanEdge childnegate = child.negate();
  84         bexpr->replaced = true;
  85         if (b0 == child) {
  86                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
  87         } else if (b0 == childnegate) {
  88                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
  89         } else if (b1 == child) {
  90                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
  91         } else if (b1 == childnegate) {
  92                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
  93         } else
  94                 ASSERT(0);
  95 }
  96
  97 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
  98         BooleanEdge childNegate=child.negate();
  99
 100         boolMap.remove(bexpr);
 101
 102         for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
 103                 BooleanEdge b = bexpr->inputs.get(i);
 104
 105                 if (b == child) {
 106                         bexpr->inputs.remove(i);
 107                         i--;
 108                 } else if (b == childNegate) {
 109                         replaceBooleanWithFalse(bexpr);
 110                         return;
 111                 }
 112         }
 113
 114         uint size=bexpr->inputs.getSize();
 115         if (size == 0) {
 116                 bexpr->replaced = true;
 117                 replaceBooleanWithTrue(bexpr);
 118         } else if (size == 1) {
 119                 bexpr->replaced = true;
 120                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
 121         } else {
 122                 //Won't build any of these in future cases...
 123                 boolMap.put(bexpr, bexpr);
 124         }
 125 }
 126
 127 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 128         replaceBooleanWithTrue(bexpr.negate());
 129 }
 130
 131 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
 132         bool isNegated=bexpr.isNegated();
 133         BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
 134         BooleanEdge result;
 135         if (b->op == SATC_IFF) {
 136                 if (isTrue(b->inputs.get(0))) {
 137                         result = b->inputs.get(1);
 138                 } else if (isFalse(b->inputs.get(0))) {
 139                         result = b->inputs.get(1).negate();
 140                 } else if (isTrue(b->inputs.get(1))) {
 141                         result = b->inputs.get(0);
 142                 } else if (isFalse(b->inputs.get(1))) {
 143                         result = b->inputs.get(0).negate();
 144                 } else ASSERT(0);
 145         } else if (b->op==SATC_AND) {
 146                 uint size = b->inputs.getSize();
 147                 if (size == 0)
 148                         result = boolTrue;
 149                 else if (size == 1)
 150                         result = b->inputs.get(0);
 151                 else ASSERT(0);
 152         }
 153         return isNegated ? result.negate() : result;
 154 }