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()));
51 if(a.var_no()>=(
unsigned)
solver->model.size())
56 if(
solver->model[a.var_no()]==l_True)
58 else if(
solver->model[a.var_no()]==l_False)
79 catch(Minisat::OutOfMemoryException)
81 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
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;
147 catch(
const Minisat::OutOfMemoryException &)
149 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
150 status = statust::ERROR;
151 throw std::bad_alloc();
167 template <
typename T>
172 log.statistics() << (no_variables() - 1) <<
" variables, "
181 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
183 status = statust::UNSAT;
184 return resultt::P_UNSATISFIABLE;
188 for(
const auto &assumption : assumptions)
190 if(assumption.is_false())
192 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
194 status = statust::UNSAT;
195 return resultt::P_UNSATISFIABLE;
199 Minisat::vec<Minisat::Lit> solver_assumptions;
200 convert(assumptions, solver_assumptions);
202 using Minisat::lbool;
206 void (*old_handler)(int) = SIG_ERR;
208 if(time_limit_seconds != 0)
212 if(old_handler == SIG_ERR)
213 log.warning() <<
"Failed to set solver time limit" <<
messaget::eom;
215 alarm(time_limit_seconds);
218 lbool solver_result =
solver->solveLimited(solver_assumptions);
220 if(old_handler != SIG_ERR)
223 signal(SIGALRM, old_handler);
229 if(time_limit_seconds != 0)
231 log.warning() <<
"Time limit ignored (not supported on Win32 yet)"
235 lbool solver_result =
solver->solve(solver_assumptions) ? l_True : l_False;
239 if(solver_result == l_True)
241 log.status() <<
"SAT checker: instance is SATISFIABLE" <<
messaget::eom;
243 status = statust::SAT;
244 return resultt::P_SATISFIABLE;
247 if(solver_result == l_False)
249 log.status() <<
"SAT checker: instance is UNSATISFIABLE" <<
messaget::eom;
250 status = statust::UNSAT;
251 return resultt::P_UNSATISFIABLE;
254 log.status() <<
"SAT checker: timed out or other error" <<
messaget::eom;
255 status = statust::ERROR;
256 return resultt::P_ERROR;
258 catch(
const Minisat::OutOfMemoryException &)
260 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
261 status=statust::ERROR;
262 return resultt::P_ERROR;
274 bool sign = a.
sign();
277 solver->model.growTo(v + 1);
279 solver->model[v] = Minisat::lbool(value);
281 catch(
const Minisat::OutOfMemoryException &)
283 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
284 status = statust::ERROR;
285 throw std::bad_alloc();
289 template <
typename T>
314 for(
int i=0; i<
solver->conflict.size(); i++)
315 if(var(
solver->conflict[i])==v)
327 for(
const auto &assumption : bv)
329 if(!assumption.is_true())
331 assumptions.push_back(assumption);
362 catch(
const Minisat::OutOfMemoryException &)
366 throw std::bad_alloc();