5 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
6 if (constraints.contains(bexpr.negate())) {
7 constraints.remove(bexpr.negate());
10 if (constraints.contains(bexpr)) {
11 constraints.remove(bexpr);
14 uint size = bexpr->parents.getSize();
15 for (uint i = 0; i < size; i++) {
16 Boolean *parent = bexpr->parents.get(i);
17 BooleanLogic *logicop = (BooleanLogic *) parent;
18 switch (logicop->op) {
20 handleANDTrue(logicop, bexpr);
23 handleIFFTrue(logicop, bexpr);
34 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
36 if (oldb.isNegated()) {
40 if (constraints.contains(oldb)) {
41 constraints.remove(oldb);
42 constraints.add(newb);
44 if (constraints.contains(oldb.negate())) {
45 constraints.remove(oldb.negate());
46 constraints.add(newb.negate());
49 BooleanEdge oldbnegated = oldb.negate();
50 uint size = oldb->parents.getSize();
51 for (uint i = 0; i < size; i++) {
52 Boolean *parent = oldb->parents.get(i);
53 BooleanLogic *logicop = (BooleanLogic *) parent;
55 uint parentsize = logicop->inputs.getSize();
57 for (uint j = 0; j < parentsize; j++) {
58 BooleanEdge b = logicop->inputs.get(i);
60 logicop->inputs.set(i, newb);
61 newb->parents.push(parent);
62 } else if (b == oldbnegated) {
63 logicop->inputs.set(i, newb.negate());
64 newb->parents.push(parent);
70 void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
71 uint size = bexpr->inputs.getSize();
72 BooleanEdge b0 = bexpr->inputs.get(0);
73 BooleanEdge b1 = bexpr->inputs.get(1);
74 BooleanEdge childnegate = child.negate();
76 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
77 } else if (b0 == childnegate) {
78 replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
79 } else if (b1 == child) {
80 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
81 } else if (b1 == childnegate) {
82 replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
87 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
88 BooleanEdge childNegate=child.negate();
90 for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
91 BooleanEdge b = bexpr->inputs.get(i);
94 bexpr->inputs.remove(i);
98 if (b == childNegate) {
99 replaceBooleanWithFalse(bexpr);
104 uint size=bexpr->inputs.getSize();
106 replaceBooleanWithTrue(bexpr);
107 } else if (size == 1) {
108 replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
112 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
113 replaceBooleanWithTrue(bexpr.negate());