23 #include <minisat/core/Solver.h>
24 #include <minisat/simp/SimpSolver.h>
27 #error "Expected HAVE_MINISAT2"
30 void convert(
const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
33 bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
34 dest.capacity(static_cast<int>(bv.size()));
38 dest.push(Minisat::mkLit(it->var_no(), it->sign()));
79 catch(Minisat::OutOfMemoryException)
82 status = statust::ERROR;
83 throw std::bad_alloc();
101 return "MiniSAT 2.2.1 without simplifier";
106 return "MiniSAT 2.2.1 with simplifier";
112 while((
unsigned)
solver->nVars()<no_variables())
127 else if(!it->is_false())
130 it->var_no() < (unsigned)
solver->nVars(),
"variable not added yet");
134 Minisat::vec<Minisat::Lit> c;
145 catch(
const Minisat::OutOfMemoryException &)
148 status = statust::ERROR;
149 throw std::bad_alloc();
172 (no_variables()-1) <<
" variables, " <<
173 solver->nClauses() <<
" clauses" << eom;
183 "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
188 bool has_false=
false;
197 "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
201 Minisat::vec<Minisat::Lit> solver_assumptions;
202 convert(assumptions, solver_assumptions);
204 using Minisat::lbool;
208 void (*old_handler)(int)=SIG_ERR;
210 if(time_limit_seconds!=0)
214 if(old_handler==SIG_ERR)
215 warning() <<
"Failed to set solver time limit" << eom;
217 alarm(time_limit_seconds);
220 lbool solver_result=
solver->solveLimited(solver_assumptions);
222 if(old_handler!=SIG_ERR)
225 signal(SIGALRM, old_handler);
231 if(time_limit_seconds!=0)
234 "Time limit ignored (not supported on Win32 yet)" <<
messaget::eom;
238 solver->solve(solver_assumptions) ? l_True : l_False;
242 if(solver_result==l_True)
245 "SAT checker: instance is SATISFIABLE" << eom;
248 return resultt::P_SATISFIABLE;
250 else if(solver_result==l_False)
253 "SAT checker: instance is UNSATISFIABLE" << eom;
258 "SAT checker: timed out or other error" << eom;
259 status=statust::ERROR;
260 return resultt::P_ERROR;
265 status=statust::UNSAT;
266 return resultt::P_UNSATISFIABLE;
268 catch(
const Minisat::OutOfMemoryException &)
271 "SAT checker ran out of memory" << eom;
272 status=statust::ERROR;
273 return resultt::P_ERROR;
285 bool sign = a.
sign();
288 solver->model.growTo(v + 1);
290 solver->model[v] = Minisat::lbool(value);
292 catch(
const Minisat::OutOfMemoryException &)
295 status = statust::ERROR;
296 throw std::bad_alloc();
302 solver(_solver), time_limit_seconds(0)
323 for(
int i=0; i<
solver->conflict.size(); i++)
324 if(var(
solver->conflict[i])==v)
363 catch(
const Minisat::OutOfMemoryException &)
367 throw std::bad_alloc();