src/AST/rewriter.cc

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