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