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 = new CSolver();
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 = solver->createSet(0, set1, 1);
27 Set *s2 = solver->createSet(0, set2, 2);
28 Set *s3 = solver->createSet(0, set3, 2);
29 Set *s4 = solver->createSet(0, set4, 3);
30 Set *s5 = solver->createSet(0, set5, 3);
31 Element *e1 = solver->getElementVar(s1);
32 Element *e2 = solver->getElementVar(s2);
33 Element *e7 = solver->getElementVar(s5);
34 BooleanEdge overflow = solver->getBooleanVar(2);
35 //change the overflow flag
36 Function *f1 = solver->createFunctionOperator(SATC_SUB, s2, SATC_IGNORE);
37 Element *in1[] = {e1, e2};
38 Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
39 Table *t1 = solver->createTable(s3);
40 uint64_t row1[] = {6, 2};
41 uint64_t row2[] = {6, 4};
42 solver->addTableEntry(t1, row1, 2, 3);
43 solver->addTableEntry(t1, row2, 2, 1);
44 Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR);
45 Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
47 Element *in2[] = {e1};
48 Table *t2 = solver->createTable(s1);
49 uint64_t row3[] = {6};
50 solver->addTableEntry(t2, row3, 1, 6);
51 Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR);
52 Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
54 Element *in3[] = {e3, e4, e5};
55 Table *t3 = solver->createTable(s4);
56 uint64_t row4[] = {4, 3, 6};
57 uint64_t row5[] = {2, 1, 6};
58 uint64_t row6[] = {2, 3, 6};
59 uint64_t row7[] = {4, 1, 6};
60 solver->addTableEntry(t3, row4, 3, 3);
61 solver->addTableEntry(t3, row5, 3, 1);
62 solver->addTableEntry(t3, row6, 3, 2);
63 solver->addTableEntry(t3, row7, 3, 1);
64 Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR);
65 Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
67 Predicate *gt = solver->createPredicateOperator(SATC_GT);
68 Element *inputs2 [] = {e7, e6};
69 BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
70 solver->addConstraint(pred);
73 if (solver->solve() == 1)
74 printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
75 solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));