From: bdemsky <bdemsky@uci.edu>
Date: Fri, 20 Oct 2017 21:28:49 +0000 (-0700)
Subject: Add test cases
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=fb8c93b8273647234690b5f02f0ef818d17944c0;hp=23d460e60a4a44a1e7dab8fe9153cad37728a20d

Add test cases
---

diff --git a/src/Test/constraint.cc b/src/Test/constraint.cc
new file mode 100644
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
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;
+}