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