Add AST Hashing and Equals Functions

[satune.git] / src / Test / tablefuncencodetest.cc

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
index a7b9412a1b54e404c7b18abc4c37bdcba21c413f..f0610e4bb28f3d10d8a48509299497f16fb6a12d 100644 (file)
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -14,46 +14,47 @@
  * Result: e1=1, e2=5, e3=7, e4=6, overflow=0
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {1, 2};
        uint64_t set2[] = {3, 5, 7};
        uint64_t set3[] = {6, 10, 19};
-       Set *s1 = createSet(solver, 0, set1, 2);
-       Set *s2 = createSet(solver, 0, set2, 3);
-       Set *s3 = createSet(solver, 0, set3, 3);
-       Element *e1 = getElementVar(solver, s1);
-       Element *e2 = getElementVar(solver, s2);
-       Element *e4 = getElementVar(solver, s3);
-       Boolean *overflow = getBooleanVar(solver, 2);
+       Set *s1 = solver->createSet(0, set1, 2);
+       Set *s2 = solver->createSet(0, set2, 3);
+       Set *s3 = solver->createSet(0, set3, 3);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
+       Element *e4 = solver->getElementVar(s3);
+       Boolean *overflow = solver->getBooleanVar(2);
        Set *d1[] = {s1, s2};
        //change the overflow flag
-       Table *t1 = createTable(solver, d1, 2, s2);
+       Table *t1 = solver->createTable(d1, 2, s2);
        uint64_t row1[] = {1, 5};
        uint64_t row2[] = {2, 3};
        uint64_t row3[] = {1, 7};
        uint64_t row4[] = {2, 7};
        uint64_t row5[] = {2, 5};
        uint64_t row6[] = {1, 3};
-       addTableEntry(solver, t1, row1, 2, 7);
-       addTableEntry(solver, t1, row2, 2, 5);
-       addTableEntry(solver, t1, row3, 2, 3);
-       addTableEntry(solver, t1, row4, 2, 5);
-       addTableEntry(solver, t1, row5, 2, 3);
-       addTableEntry(solver, t1, row6, 2, 5);
-       Function *f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);
-       Element *e3 = applyFunction(solver, f1, (Element * []) {e1,e2}, 2, overflow);
+       solver->addTableEntry(t1, row1, 2, 7);
+       solver->addTableEntry(t1, row2, 2, 5);
+       solver->addTableEntry(t1, row3, 2, 3);
+       solver->addTableEntry(t1, row4, 2, 5);
+       solver->addTableEntry(t1, row5, 2, 3);
+       solver->addTableEntry(t1, row6, 2, 5);
+       Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED);
+       Element *tmparray[] = {e1, e2};
+       Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
 
        Set *deq[] = {s3,s2};
-       Predicate *lte = createPredicateOperator(solver, LTE, deq, 2);
+       Predicate *lte = solver->createPredicateOperator(LTE, deq, 2);
        Element *inputs2 [] = {e4, e3};
-       Boolean *pred = applyPredicate(solver, lte, inputs2, 2);
-       addConstraint(solver, pred);
+       Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
+       solver->addConstraint(pred);
 
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu e3=%llu e4=%llu overFlow:%d\n",
-                                        getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e3),
-                                        getElementValue(solver, e4), getBooleanValue(solver, overflow));
+       if (solver->startEncoding() == 1)
+               printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n",
+                                        solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3),
+                                        solver->getElementValue(e4), solver->getBooleanValue(overflow));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }