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