src/AST/rewriter.cc

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