3 int main(int numargs, char **argv) {
4 CSolver *solver = new CSolver();
5 uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
6 Set *s = solver->createSet(0, set1, 8);
7 Order *order = solver->createOrder(SATC_TOTAL, s);
8 BooleanEdge o12 = solver->orderConstraint(order, 1, 2);
9 BooleanEdge o13 = solver->orderConstraint(order, 1, 3);
10 BooleanEdge o24 = solver->orderConstraint(order, 2, 4);
11 BooleanEdge o34 = solver->orderConstraint(order, 3, 4);
12 BooleanEdge o41 = solver->orderConstraint(order, 4, 1);
13 BooleanEdge o57 = solver->orderConstraint(order, 5, 7);
14 BooleanEdge o76 = solver->orderConstraint(order, 7, 6);
15 BooleanEdge o65 = solver->orderConstraint(order, 6, 5);
16 BooleanEdge o58 = solver->orderConstraint(order, 5, 8);
17 BooleanEdge o81 = solver->orderConstraint(order, 8, 1);
19 BooleanEdge array1[] = {o12, o13, o24, o34};
20 solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );
21 BooleanEdge array2[] = {o41, o57};
23 BooleanEdge b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
24 BooleanEdge array3[] = {o34};
25 BooleanEdge o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
26 BooleanEdge array4[] = {o24};
27 BooleanEdge o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
28 BooleanEdge array5[] = {o34n, o24n};
29 BooleanEdge b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
30 BooleanEdge array6[] = {b1, b2};
31 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
33 BooleanEdge array7[] = {o12, o13};
34 solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
36 BooleanEdge array8[] = {o76, o65};
37 solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
39 BooleanEdge array9[] = {o76, o65};
40 BooleanEdge b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
41 BooleanEdge array10[] = {o57};
42 BooleanEdge o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
43 BooleanEdge array11[] = {b3, o57n};
44 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
46 BooleanEdge array12[] = {o58, o81};
47 solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
49 /* if (solver->solve() == 1)
54 solver->autoTune(100);