From 42e411a9054f33603b8f0b8f2478d449e6484a1e Mon Sep 17 00:00:00 2001 From: Hamed Date: Mon, 10 Jul 2017 16:46:11 -0700 Subject: [PATCH] SAT solver is now connected to csolver --- src/Test/run.sh | 2 ++ src/csolver.c | 6 ++---- 2 files changed, 4 insertions(+), 4 deletions(-) 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); -- 2.34.1