Add test cases

diff --git a/src/Test/constraint.cc b/src/Test/constraint.cc
new file mode 100644 (file)
index 0000000..60dd586
--- /dev/null
+++ b/src/Test/constraint.cc
@@ -0,0 +1,21 @@
+#include "csolver.h"
+
+int main(int numargs, char **argv) {
+       CSolver *solver = new CSolver();
+       uint64_t elements[]={0, 1};
+       Set * s = solver->createSet(1, elements, 2);
+       Element * e1=solver->getElementVar(s);
+       Element * e2=solver->getElementVar(s);
+       Set * sarray[]={s, s};
+       Predicate *p=solver->createPredicateOperator(SATC_LT, sarray, 2);
+       Element *earray[]={e1, e2};
+       BooleanEdge be=solver->applyPredicate(p, earray, 2);
+       solver->addConstraint(be);
+
+       if (solver->solve() == 1) {
+               printf("SAT\n");
+       } else {
+               printf("UNSAT\n");
+       }
+       delete solver;
+}

diff --git a/src/Test/graphtest.cc b/src/Test/graphtest.cc
new file mode 100644 (file)
index 0000000..976ce60
--- /dev/null
+++ b/src/Test/graphtest.cc
@@ -0,0 +1,19 @@
+#include "csolver.h"
+
+int main(int numargs, char **argv) {
+       CSolver *solver = new CSolver();
+       uint64_t set1[] = {1, 2, 3};
+       Set *s = solver->createSet(0, set1, 3);
+       Order *order = solver->createOrder(SATC_TOTAL, s);
+       BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
+       solver->addConstraint(b12);
+       BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
+       solver->addConstraint(b23);
+
+       if (solver->solve() == 1) {
+               printf("SAT\n");
+       } else {
+               printf("UNSAT\n");
+       }
+       delete solver;
+}