Breaking Multituner into comptuner and kmeanstuner

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

diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc
index 5cbdd0460435a8cc52fa6b6b413c64b9d66082e4..e179bae74f49fbf483b74dfc62b8ceef7f22df91 100644 (file)
--- a/src/Test/elemequalunsattest.cc
+++ b/src/Test/elemequalunsattest.cc
@@ -7,22 +7,21 @@
  * Result: UNSAT
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {0, 1, 2};
        uint64_t set2[] = {3, 4};
-       Set *s1 = createSet(solver, 0, set1, 3);
-       Set *s2 = createSet(solver, 0, set2, 2);
-       Element *e1 = getElementVar(solver, s1);
-       Element *e2 = getElementVar(solver, s2);
-       Set *domain[] = {s1, s2};
-       Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+       Set *s1 = solver->createSet(0, set1, 3);
+       Set *s2 = solver->createSet(0, set2, 2);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
-       Boolean *b = applyPredicate(solver, equals, inputs, 2);
-       addConstraint(solver, b);
-
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+       BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
+       solver->addConstraint(b);
+       solver->serialize();
+       if (solver->solve() == 1)
+               printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }