7 * Result: b1=1 b2=0 b3=0 b4=0
9 int main(int numargs, char **argv) {
10 CSolver *solver = new CSolver();
11 BooleanEdge b1 = solver->getBooleanVar(0);
12 BooleanEdge b2 = solver->getBooleanVar(0);
13 BooleanEdge b3 = solver->getBooleanVar(0);
14 BooleanEdge b4 = solver->getBooleanVar(0);
15 //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
16 BooleanEdge barray1[] = {b1,b2};
17 BooleanEdge andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
18 BooleanEdge barray2[] = {andb1b2, b3};
19 BooleanEdge imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);
20 solver->addConstraint(imply);
21 BooleanEdge barray3[] = {b3};
22 BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
23 BooleanEdge barray4[] = {notb3, b4};
24 solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
25 BooleanEdge barray5[] = {b1, b4};
26 solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
28 if (solver->solve() == 1)
29 printf("b1=%d b2=%d b3=%d b4=%d\n",
30 solver->getBooleanValue(b1), solver->getBooleanValue(b2),
31 solver->getBooleanValue(b3), solver->getBooleanValue(b4));