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);