Preprocess bug fix
[satune.git] / src / Test / funcencodingtest.cc
index e3baeb95799c8f81d53e4152834fa1f93bad9bf9..a6a482a7d5d4d39d2239a7ce072d5e596708cd16 100644 (file)
@@ -32,12 +32,11 @@ int main(int numargs, char **argv) {
        Element *e2 = solver->getElementVar(s2);
        Element *e7 = solver->getElementVar(s5);
        BooleanEdge overflow = solver->getBooleanVar(2);
-       Set *d1[] = {s1, s2};
        //change the overflow flag
-       Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE);
+       Function *f1 = solver->createFunctionOperator(SATC_SUB, s2, SATC_IGNORE);
        Element *in1[] = {e1, e2};
        Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
-       Table *t1 = solver->createTable(d1, 2, s3);
+       Table *t1 = solver->createTable(s3);
        uint64_t row1[] = {6, 2};
        uint64_t row2[] = {6, 4};
        solver->addTableEntry(t1, row1, 2, 3);
@@ -45,17 +44,15 @@ int main(int numargs, char **argv) {
        Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR);
        Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
 
-       Set *d2[] = {s1};
        Element *in2[] = {e1};
-       Table *t2 = solver->createTable(d2, 1, s1);
+       Table *t2 = solver->createTable(s1);
        uint64_t row3[] = {6};
        solver->addTableEntry(t2, row3, 1, 6);
        Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR);
        Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
 
-       Set *d3[] = {s2, s3, s1};
        Element *in3[] = {e3, e4, e5};
-       Table *t3 = solver->createTable(d3, 3, s4);
+       Table *t3 = solver->createTable(s4);
        uint64_t row4[] = {4, 3, 6};
        uint64_t row5[] = {2, 1, 6};
        uint64_t row6[] = {2, 3, 6};
@@ -67,11 +64,11 @@ int main(int numargs, char **argv) {
        Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR);
        Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
 
-       Set *deq[] = {s5,s4};
-       Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2);
+       Predicate *gt = solver->createPredicateOperator(SATC_GT);
        Element *inputs2 [] = {e7, e6};
        BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
        solver->addConstraint(pred);
+       solver->serialize();
 
        if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",