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