5 * e3=Fsub(e1,e2) {4, 2}
10 * e6 = (e3, e4, e5) {2, 3, 1}
17 * Result: e1=6, e2=4, e7=2
19 int main(int numargs, char **argv) {
20 CSolver *solver = allocCSolver();
21 uint64_t set1[] = {6};
22 uint64_t set2[] = {4, 2};
23 uint64_t set3[] = {3, 1};
24 uint64_t set4[] = {2, 3, 1};
25 uint64_t set5[] = {2, 1, 0};
26 Set *s1 = createSet(solver, 0, set1, 1);
27 Set *s2 = createSet(solver, 0, set2, 2);
28 Set *s3 = createSet(solver, 0, set3, 2);
29 Set *s4 = createSet(solver, 0, set4, 3);
30 Set *s5 = createSet(solver, 0, set5, 3);
31 Element *e1 = getElementVar(solver, s1);
32 Element *e2 = getElementVar(solver, s2);
33 Element *e7 = getElementVar(solver, s5);
34 Boolean *overflow = getBooleanVar(solver, 2);
36 //change the overflow flag
37 Function *f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
38 Element *in1[] = {e1, e2};
39 Element *e3 = applyFunction(solver, f1, in1, 2, overflow);
40 Table *t1 = createTable(solver, d1, 2, s3);
41 uint64_t row1[] = {6, 2};
42 uint64_t row2[] = {6, 4};
43 addTableEntry(solver, t1, row1, 2, 3);
44 addTableEntry(solver, t1, row2, 2, 1);
45 Function *f2 = completeTable(solver, t1, IGNOREBEHAVIOR);
46 Element *e4 = applyFunction(solver, f2, in1, 2, overflow);
49 Element *in2[] = {e1};
50 Table *t2 = createTable(solver, d2, 1, s1);
51 uint64_t row3[] = {6};
52 addTableEntry(solver, t2, row3, 1, 6);
53 Function *f3 = completeTable(solver, t2, IGNOREBEHAVIOR);
54 Element *e5 = applyFunction(solver, f3, in2, 1, overflow);
56 Set *d3[] = {s2, s3, s1};
57 Element *in3[] = {e3, e4, e5};
58 Table *t3 = createTable(solver, d3, 3, s4);
59 uint64_t row4[] = {4, 3, 6};
60 uint64_t row5[] = {2, 1, 6};
61 uint64_t row6[] = {2, 3, 6};
62 uint64_t row7[] = {4, 1, 6};
63 addTableEntry(solver, t3, row4, 3, 3);
64 addTableEntry(solver, t3, row5, 3, 1);
65 addTableEntry(solver, t3, row6, 3, 2);
66 addTableEntry(solver, t3, row7, 3, 1);
67 Function *f4 = completeTable(solver, t3, IGNOREBEHAVIOR);
68 Element *e6 = applyFunction(solver, f4, in3, 3, overflow);
71 Predicate *gt = createPredicateOperator(solver, GT, deq, 2);
72 Element *inputs2 [] = {e7, e6};
73 Boolean *pred = applyPredicate(solver, gt, inputs2, 2);
74 addConstraint(solver, pred);
76 if (startEncoding(solver) == 1)
77 printf("e1=%llu e2=%llu e7=%llu\n",
78 getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));