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