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_OR:
  19                         replaceBooleanWithTrue(parent);
  20                         break;
  21                 case SATC_NOT:
  22                         replaceBooleanWithFalse(parent);
  23                         break;
  24                 case SATC_IFF:
  25                         handleXORFalse(logicop, bexpr);
  26                         break;
  27                 case SATC_XOR:
  28                         handleXORTrue(logicop, bexpr);
  29                         break;
  30                 case SATC_IMPLIES:
  31                         handleIMPLIESTrue(logicop, bexpr);
  32                         break;
  33                 }
  34         }
  35 }
  36
  37 void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
  38         if (constraints.contains(oldb)) {
  39                 constraints.remove(oldb);
  40                 constraints.add(newb);
  41         }
  42
  43         uint size = oldb->parents.getSize();
  44         for (uint i = 0; i < size; i++) {
  45                 Boolean *parent = oldb->parents.get(i);
  46                 BooleanLogic *logicop = (BooleanLogic *) parent;
  47
  48                 uint parentsize = logicop->inputs.getSize();
  49
  50                 for (uint j = 0; j < parentsize; j++) {
  51                         Boolean *b = logicop->inputs.get(i);
  52                         if (b == oldb) {
  53                                 logicop->inputs.set(i, newb);
  54                                 newb->parents.push(parent);
  55                         }
  56                 }
  57         }
  58 }
  59
  60 void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
  61         uint size = bexpr->inputs.getSize();
  62         Boolean *b = bexpr->inputs.get(0);
  63         uint childindex = (b == child) ? 0 : 1;
  64         bexpr->inputs.remove(childindex);
  65         bexpr->op = SATC_NOT;
  66 }
  67
  68 void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
  69         uint size = bexpr->inputs.getSize();
  70         Boolean *b = bexpr->inputs.get(0);
  71         uint otherindex = (b == child) ? 1 : 0;
  72         replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
  73 }
  74
  75 void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
  76         uint size = bexpr->inputs.getSize();
  77         Boolean *b = bexpr->inputs.get(0);
  78         if (b == child) {
  79                 //Replace with other term
  80                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
  81         } else {
  82                 //Statement is true...
  83                 replaceBooleanWithTrue(bexpr);
  84         }
  85 }
  86
  87 void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
  88         uint size = bexpr->inputs.getSize();
  89         Boolean *b = bexpr->inputs.get(0);
  90         if (b == child) {
  91                 //Statement is true...
  92                 replaceBooleanWithTrue(bexpr);
  93         } else {
  94                 //Make into negation of first term
  95                 bexpr->inputs.get(1);
  96                 bexpr->op = SATC_NOT;
  97         }
  98 }
  99
 100 void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
 101         uint size = bexpr->inputs.getSize();
 102
 103         if (size == 1) {
 104                 replaceBooleanWithTrue(bexpr);
 105                 return;
 106         }
 107
 108         for (uint i = 0; i < size; i++) {
 109                 Boolean *b = bexpr->inputs.get(i);
 110                 if (b == child) {
 111                         bexpr->inputs.remove(i);
 112                 }
 113         }
 114
 115         if (size == 2) {
 116                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
 117         }
 118 }
 119
 120 void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
 121         uint size = bexpr->inputs.getSize();
 122
 123         if (size == 1) {
 124                 replaceBooleanWithFalse(bexpr);
 125         }
 126
 127         for (uint i = 0; i < size; i++) {
 128                 Boolean *b = bexpr->inputs.get(i);
 129                 if (b == child) {
 130                         bexpr->inputs.remove(i);
 131                 }
 132         }
 133
 134         if (size == 2) {
 135                 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
 136         }
 137 }
 138
 139 void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
 140         if (constraints.contains(bexpr)) {
 141                 setUnSAT();
 142                 constraints.remove(bexpr);
 143         }
 144
 145         uint size = bexpr->parents.getSize();
 146         for (uint i = 0; i < size; i++) {
 147                 Boolean *parent = bexpr->parents.get(i);
 148                 BooleanLogic *logicop = (BooleanLogic *) parent;
 149                 switch (logicop->op) {
 150                 case SATC_AND:
 151                         replaceBooleanWithFalse(parent);
 152                         break;
 153                 case SATC_OR:
 154                         handleORFalse(logicop, bexpr);
 155                         break;
 156                 case SATC_NOT:
 157                         replaceBooleanWithTrue(parent);
 158                         break;
 159                 case SATC_IFF:
 160                         handleXORTrue(logicop, bexpr);
 161                         break;
 162                 case SATC_XOR:
 163                         handleXORFalse(logicop, bexpr);
 164                         break;
 165                 case SATC_IMPLIES:
 166                         handleIMPLIESFalse(logicop, bexpr);
 167                         break;
 168                 }
 169         }
 170 }