src/AST/rewriter.cc

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