From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 02:26:37 +0000 (-0700)
Subject: Extend test case to call solver
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=93ce78ab3fd349ab5207c482f11685e2101d3736;p=satune.git

Extend test case to call solver
---

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index a6d9dcc..340cdd0 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -19,7 +19,8 @@ CNF * createCNF() {
 	cnf->enableMatching=true;
 	allocInlineDefVectorEdge(& cnf->constraints);
 	allocInlineDefVectorEdge(& cnf->args);
- return cnf;
+	cnf->solver=allocIncrementalSolver();
+	return cnf;
 }
 
 void deleteCNF(CNF * cnf) {
@@ -30,6 +31,7 @@ void deleteCNF(CNF * cnf) {
 	}
 	deleteVectorArrayEdge(& cnf->constraints);
 	deleteVectorArrayEdge(& cnf->args);
+	deleteIncrementalSolver(cnf->solver);
 	ourfree(cnf->node_array);
 	ourfree(cnf);
 }
@@ -275,6 +277,13 @@ Edge constraintNewVar(CNF *cnf) {
 	return e;
 }
 
+void solveCNF(CNF *cnf) {
+	countPass(cnf);
+	convertPass(cnf, false);
+	solve(cnf->solver);
+}
+
+
 void countPass(CNF *cnf) {
 	uint numConstraints=getSizeVectorEdge(&cnf->constraints);
 	VectorEdge *ve=allocDefVectorEdge();
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index aff2c35..95ee530 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -191,7 +191,7 @@ Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 void addConstraint(CNF *cnf, Edge constraint);
-
+void solveCNF(CNF *cnf);
 
 
 void convertPass(CNF *cnf, bool backtrackLit);
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 68e2104..82f926d 100644
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -12,5 +12,6 @@ int main(int numargs, char ** argv) {
 	Edge iff3=constraintIFF(cnf, v3, nv1);
 	Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
 	addConstraint(cnf, cand);
+	solveCNF(cnf);
 	deleteCNF(cnf);
 }