Bug fix

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

diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc
index 4818f246e90cb1aff667d00a9d986993b909b182..74b456963a87e6c73c96f82b0f305d10965ed84e 100644 (file)
--- a/src/Test/ltelemconsttest.cc
+++ b/src/Test/ltelemconsttest.cc
@@ -6,21 +6,19 @@
  * Result: e1=5 e2=6
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
-       uint64_t set1[] = {5};
+       CSolver *solver = new CSolver();
        uint64_t set3[] = {1, 3, 4, 6};
-       Set *s1 = createSet(solver, 0, set1, 3);
-       Set *s3 = createSet(solver, 0, set3, 4);
-       Element *e1 = getElementConst(solver, 4, 5);
-       Element *e2 = getElementVar(solver, s3);
-       Set *domain2[] = {s1, s3};
-       Predicate *lt = createPredicateOperator(solver, LT, domain2, 2);
+       Set *s3 = solver->createSet(0, set3, 4);
+       Element *e1 = solver->getElementConst(4, 5);
+       Element *e2 = solver->getElementVar(s3);
+       Predicate *lt = solver->createPredicateOperator(SATC_LT);
        Element *inputs2[] = {e1, e2};
-       Boolean *b = applyPredicate(solver, lt, inputs2, 2);
-       addConstraint(solver, b);
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+       BooleanEdge b = solver->applyPredicate(lt, inputs2, 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);
-}
\ No newline at end of file
+       delete solver;
+}