7 * Result: b1=1 b2=0 b3=0 b4=0
9 int main(int numargs, char **argv) {
10 CSolver *solver = allocCSolver();
11 Boolean *b1 = getBooleanVar(solver, 0);
12 Boolean *b2 = getBooleanVar(solver, 0);
13 Boolean *b3 = getBooleanVar(solver, 0);
14 Boolean *b4 = getBooleanVar(solver, 0);
15 //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
16 Boolean * barray1[]={b1,b2};
17 Boolean *andb1b2 = applyLogicalOperation(solver, L_AND, barray1, 2);
18 Boolean * barray2[]={andb1b2, b3};
19 Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, barray2, 2);
20 addConstraint(solver, imply);
21 Boolean * barray3[] ={b3};
22 Boolean *notb3 = applyLogicalOperation(solver, L_NOT, barray3, 1);
23 Boolean * barray4[] ={notb3, b4};
24 addConstraint(solver, applyLogicalOperation(solver, L_OR, barray4, 2));
25 Boolean * barray5[] ={b1, b4};
26 addConstraint(solver, applyLogicalOperation(solver, L_XOR, barray5, 2));
27 if (startEncoding(solver) == 1)
28 printf("b1=%d b2=%d b3=%d b4=%d\n",
29 getBooleanValue(solver,b1), getBooleanValue(solver, b2),
30 getBooleanValue(solver, b3), getBooleanValue(solver, b4));