renaming
[satune.git] / 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_XOR:
25                         handleXORTrue(logicop, bexpr);
26                         break;
27                 case SATC_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 = SATC_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 = SATC_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 SATC_AND:
148                         replaceBooleanWithFalse(parent);
149                         break;
150                 case SATC_OR:
151                         handleORFalse(logicop, bexpr);
152                         break;
153                 case SATC_NOT:
154                         replaceBooleanWithTrue(parent);
155                         break;
156                 case SATC_XOR:
157                         handleXORFalse(logicop, bexpr);
158                         break;
159                 case SATC_IMPLIES:
160                         handleIMPLIESFalse(logicop, bexpr);
161                         break;
162                 }
163         }
164 }