SAT solver is now connected to csolver
authorHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 23:46:11 +0000 (16:46 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 23:46:11 +0000 (16:46 -0700)
src/Test/run.sh
src/csolver.c

index 9741fe0..e74b557 100755 (executable)
@@ -3,5 +3,7 @@
 export LD_LIBRARY_PATH=../bin
 # For Mac OSX
 export DYLD_LIBRARY_PATH=../bin
+# For sat_solver
+export PATH=.:$PATH
 
 $@
index 985122f..e3850d1 100644 (file)
@@ -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);