From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 10 Jul 2017 23:46:11 +0000 (-0700)
Subject: SAT solver is now connected to csolver
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=42e411a9054f33603b8f0b8f2478d449e6484a1e;p=satune.git

SAT solver is now connected to csolver
---

diff --git a/src/Test/run.sh b/src/Test/run.sh
index 9741fe0..e74b557 100755
--- a/src/Test/run.sh
+++ b/src/Test/run.sh
@@ -3,5 +3,7 @@
 export LD_LIBRARY_PATH=../bin
 # For Mac OSX
 export DYLD_LIBRARY_PATH=../bin
+# For sat_solver
+export PATH=.:$PATH
 
 $@
diff --git a/src/csolver.c b/src/csolver.c
index 985122f..e3850d1 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,13 +174,11 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
 void startEncoding(CSolver* solver){
 	naiveEncodingDecision(solver);
 	SATEncoder* satEncoder = allocSATEncoder();
-	createSolver(satEncoder->satSolver);
+	satEncoder->satSolver =allocIncrementalSolver();
 	encodeAllSATEncoder(solver, satEncoder);
 	finishedClauses(satEncoder->satSolver);
-	solve(satEncoder->satSolver);
-	int result= getSolution(satEncoder->satSolver);
+	int result= solve(satEncoder->satSolver);
 	model_print("sat_solver's result:%d\n", result);
-	killSolver(satEncoder->satSolver);
 	//For now, let's just delete it, and in future for doing queries 
 	//we may need it.
 	deleteSATEncoder(satEncoder);