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