15 * Result: e1=1, e2=1, e3=6 OR 10 OR 19, overflow=1
17 int main(int numargs, char **argv) {
18 CSolver *solver = allocCSolver();
19 uint64_t set1[] = {1, 2};
20 uint64_t set2[] = {1, 3, 5, 7};
21 uint64_t set3[] = {6, 10, 19};
22 Set *s1 = createSet(solver, 0, set1, 2);
23 Set *s2 = createSet(solver, 0, set2, 4);
24 Set *s3 = createSet(solver, 0, set3, 3);
25 Element *e1 = getElementVar(solver, s1);
26 Element *e2 = getElementVar(solver, s2);
27 Element *e3 = getElementVar(solver, s3);
28 Set *d2[] = {s1, s2, s3};
29 //change the overflow flag
30 Table *t1 = createTableForPredicate(solver, d2, 3);
31 uint64_t row1[] = {1, 5, 6};
32 uint64_t row2[] = {2, 3, 19};
33 uint64_t row3[] = {1, 3, 19};
34 uint64_t row4[] = {2, 7, 10};
35 uint64_t row5[] = {1, 7, 6};
36 uint64_t row6[] = {2, 5, 6};
37 addTableEntry(solver, t1, row1, 3, true);
38 addTableEntry(solver, t1, row2, 3, true);
39 addTableEntry(solver, t1, row3, 3, false);
40 addTableEntry(solver, t1, row4, 3, false);
41 addTableEntry(solver, t1, row5, 3, false);
42 addTableEntry(solver, t1, row6, 3, true);
43 Predicate *p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED);
44 Boolean *undef = getBooleanVar(solver, 2);
45 Element * tmparray[] = {e1, e2, e3};
46 Boolean *b1 = applyPredicateTable(solver, p1, tmparray, 3, undef);
47 addConstraint(solver, b1);
50 Predicate *gte = createPredicateOperator(solver, GTE, deq, 2);
51 Element *inputs2 [] = {e3, e2};
52 Boolean *pred = applyPredicate(solver, gte, inputs2, 2);
53 addConstraint(solver, pred);
56 Predicate *eq = createPredicateOperator(solver, EQUALS, d1, 2);
57 Element * tmparray2[] = {e1, e2};
58 Boolean *pred2 = applyPredicate(solver, eq, tmparray2, 2);
59 addConstraint(solver, pred2);
61 if (startEncoding(solver) == 1)
62 printf("e1=%llu e2=%llu e3=%llu undefFlag:%d\n",
63 getElementValue(solver,e1), getElementValue(solver, e2),
64 getElementValue(solver, e3), getBooleanValue(solver, undef));