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