src/AST/rewriter.cc

   1 #include "rewriter.h"
   2 #include "boolean.h"
   3 #include "csolver.h"
   4
   5 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
   6         if (constraints.contains(bexpr.negate())) {
   7                 constraints.remove(bexpr.negate());
   8                 setUnSAT();
   9         }
  10         if (constraints.contains(bexpr)) {
  11                 constraints.remove(bexpr);
  12         }
  13
  14         replaceBooleanWithTrueNoRemove(bexpr);
  15 }
  16
  17 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
  18         uint size = bexpr->parents.getSize();
  19         for (uint i = 0; i < size; i++) {
  20                 Boolean *parent = bexpr->parents.get(i);
  21                 BooleanLogic *logicop = (BooleanLogic *) parent;
  22                 switch (logicop->op) {
  23                 case SATC_AND:
  24                         handleANDTrue(logicop, bexpr);
  25                         break;
  26                 case SATC_IFF:
  27                         handleIFFTrue(logicop, bexpr);
  28                         break;
  29                 case SATC_NOT:
  30                 case SATC_OR:
  31                 case SATC_XOR:
  32                 case SATC_IMPLIES:
  33                         ASSERT(0);
  34                 }
  35         }
  36 }
  37
  38 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
  39         //Canonicalize
  40         if (oldb.isNegated()) {
  41                 oldb=oldb.negate();
  42                 newb=newb.negate();
  43         }
  44         if (constraints.contains(oldb)) {
  45                 constraints.remove(oldb);
  46                 constraints.add(newb);
  47         }
  48         if (constraints.contains(oldb.negate())) {
  49                 constraints.remove(oldb.negate());
  50                 constraints.add(newb.negate());
  51         }
  52
  53         BooleanEdge oldbnegated = oldb.negate();
  54         uint size = oldb->parents.getSize();
  55         for (uint i = 0; i < size; i++) {
  56                 Boolean *parent = oldb->parents.get(i);
  57                 BooleanLogic *logicop = (BooleanLogic *) parent;
  58
  59                 uint parentsize = logicop->inputs.getSize();
  60
  61                 for (uint j = 0; j < parentsize; j++) {
  62                         BooleanEdge b = logicop->inputs.get(i);
  63                         if (b == oldb) {
  64                                 logicop->inputs.set(i, newb);
  65                                 newb->parents.push(parent);
  66                         } else if (b == oldbnegated) {
  67                                 logicop->inputs.set(i, newb.negate());
  68                                 newb->parents.push(parent);
  69                         }
  70                 }
  71         }
  72 }
  73
  74 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
  75         uint size = bexpr->inputs.getSize();
  76         BooleanEdge b0 = bexpr->inputs.get(0);
  77         BooleanEdge b1 = bexpr->inputs.get(1);
  78         BooleanEdge childnegate = child.negate();
  79         if (b0 == child) {
  80                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
  81         } else if (b0 == childnegate) {
  82                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
  83         } else if (b1 == child) {
  84                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
  85         } else if (b1 == childnegate) {
  86                 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
  87         } else
  88                 ASSERT(0);
  89 }
  90
  91 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
  92         BooleanEdge childNegate=child.negate();
  93
  94         for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
  95                 BooleanEdge b = bexpr->inputs.get(i);
  96
  97                 if (b == child) {
  98                         bexpr->inputs.remove(i);
  99                         i--;
 100                 }
 101
 102                 if (b == childNegate) {
 103                         replaceBooleanWithFalse(bexpr);
 104                         return;
 105                 }
 106         }
 107
 108         uint size=bexpr->inputs.getSize();
 109         if (size == 0) {
 110                 replaceBooleanWithTrue(bexpr);
 111         } else if (size == 1) {
 112                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
 113         }
 114 }
 115
 116 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 117         replaceBooleanWithTrue(bexpr.negate());
 118 }