3 int main(int numargs, char ** argv) {
4 CSolver * solver=allocCSolver();
6 uint64_t set2[]={4, 2};
7 uint64_t set3[]={3, 1};
8 uint64_t set4[]={2, 3, 1};
9 uint64_t set5[]={2, 1, 0};
10 Set * s1=createSet(solver, 0, set1, 1);
11 Set * s2=createSet(solver, 0, set2, 2);
12 Set * s3=createSet(solver, 0, set3, 2);
13 Set * s4=createSet(solver, 0, set4, 3);
14 Set * s5=createSet(solver, 0, set5, 3);
15 Element * e1=getElementVar(solver, s1);
16 Element * e2=getElementVar(solver, s2);
17 Element * e7=getElementVar(solver, s5);
18 Boolean* overflow = getBooleanVar(solver , 2);
20 //change the overflow flag
21 Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
22 Element * in1[]={e1, e2};
23 Element * e3 = applyFunction(solver, f1, in1, 2, overflow);
24 Table* t1 = createTable(solver, d1, 2, s3);
25 uint64_t row1[] = {6, 2};
26 uint64_t row2[] = {6, 4};
27 addTableEntry(solver, t1, row1, 2, 3);
28 addTableEntry(solver, t1, row2, 2, 1);
29 Function * f2 = completeTable(solver, t1);
30 Element * e4 = applyFunction(solver, f2, in1, 2, overflow);
34 Table* t2 = createTable(solver, d2, 1, s1);
35 uint64_t row3[] = {6};
36 addTableEntry(solver, t2, row3, 1, 6);
37 Function * f3 = completeTable(solver, t2);
38 Element * e5 = applyFunction(solver, f3, in2, 1, overflow);
40 Set *d3[] = {s2, s3, s1};
41 Element *in3[]={e3, e4, e5};
42 Table* t3 = createTable(solver, d3, 3, s4);
43 uint64_t row4[] = {4, 3, 6};
44 uint64_t row5[] = {2, 1, 6};
45 uint64_t row6[] = {2, 3, 6};
46 uint64_t row7[] = {4, 1, 6};
47 addTableEntry(solver, t3, row4, 3, 3);
48 addTableEntry(solver, t3, row5, 3, 1);
49 addTableEntry(solver, t3, row6, 3, 2);
50 addTableEntry(solver, t3, row7, 3, 1);
51 Function * f4 = completeTable(solver, t3);
52 Element * e6 = applyFunction(solver, f4, in3, 3, overflow);
55 Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
56 Element* inputs2 [] = {e7, e6};
57 Boolean* pred = applyPredicate(solver, gt, inputs2, 2);
58 addConstraint(solver, pred);
60 if (startEncoding(solver)==1)
61 printf("e1=%llu e2=%llu e7=%llu\n",
62 getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));