5 void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
6 if (constraints.contains(bexpr)) {
7 constraints.remove(bexpr);
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) {
16 handleANDTrue(logicop, bexpr);
19 replaceBooleanWithTrue(parent);
22 replaceBooleanWithFalse(parent);
25 handleXORTrue(logicop, bexpr);
28 handleIMPLIESTrue(logicop, bexpr);
34 void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
35 if (constraints.contains(oldb)) {
36 constraints.remove(oldb);
37 constraints.add(newb);
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;
45 uint parentsize = logicop->inputs.getSize();
47 for (uint j = 0; j < parentsize; j++) {
48 Boolean *b = logicop->inputs.get(i);
50 logicop->inputs.set(i, newb);
51 newb->parents.push(parent);
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);
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));
72 void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
73 uint size = bexpr->inputs.getSize();
74 Boolean *b = bexpr->inputs.get(0);
76 //Replace with other term
77 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
79 //Statement is true...
80 replaceBooleanWithTrue(bexpr);
84 void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
85 uint size = bexpr->inputs.getSize();
86 Boolean *b = bexpr->inputs.get(0);
88 //Statement is true...
89 replaceBooleanWithTrue(bexpr);
91 //Make into negation of first term
97 void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
98 uint size = bexpr->inputs.getSize();
101 replaceBooleanWithTrue(bexpr);
105 for (uint i = 0; i < size; i++) {
106 Boolean *b = bexpr->inputs.get(i);
108 bexpr->inputs.remove(i);
113 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
117 void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
118 uint size = bexpr->inputs.getSize();
121 replaceBooleanWithFalse(bexpr);
124 for (uint i = 0; i < size; i++) {
125 Boolean *b = bexpr->inputs.get(i);
127 bexpr->inputs.remove(i);
132 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
136 void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
137 if (constraints.contains(bexpr)) {
139 constraints.remove(bexpr);
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) {
148 replaceBooleanWithFalse(parent);
151 handleORFalse(logicop, bexpr);
154 replaceBooleanWithTrue(parent);
157 handleXORFalse(logicop, bexpr);
160 handleIMPLIESFalse(logicop, bexpr);