SAT solver is now connected to csolver

diff --git a/src/Test/run.sh b/src/Test/run.sh
index 9741fe097acd733c1f8256fc91dd615aad844cbd..e74b557af516008fcecb3684c8450d2af9e13fa0 100755 (executable)
--- 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 985122fc96400948ed543a2306abefba924c289b..e3850d15a8782cf90ae812dccddf411e7af49245 100644 (file)
--- 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);