Adding the c wrapper for CSolver
[satune.git] / src / Test / elemequalsattest.cc
index 7841a70eda242ce46789730372c420fc2e2c847d..e041cb0a1dd2155a689cdcb69d070e800657f518 100644 (file)
  *     e1=2 e2=7
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {0, 1, 2};
        uint64_t set2[] = {3, 1, 7};
-       Set *s1 = createSet(solver, 0, set1, 3);
-       Set *s2 = createSet(solver, 0, set2, 3);
-       Element *e1 = getElementVar(solver, s1);
-       Element *e2 = getElementVar(solver, s2);
+       Set *s1 = solver->createSet(0, set1, 3);
+       Set *s2 = solver->createSet(0, set2, 3);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
        Set *domain[] = {s1, s2};
-       Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
-       Boolean *b = applyPredicate(solver, equals, inputs, 2);
-       addConstraint(solver, b);
+       BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
+       solver->addConstraint(b);
+       solver->serialize();
 
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+       if (solver->solve() == 1)
+               printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }