22 #include <minisat/core/Solver.h>
23 #include <minisat/simp/SimpSolver.h>
26 #error "Expected HAVE_MINISAT2"
29 void convert(
const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
32 bv.size() <=
static_cast<std::size_t
>(std::numeric_limits<int>::max()));
33 dest.capacity(
static_cast<int>(bv.size()));
35 for(
const auto &literal : bv)
37 if(!literal.is_false())
38 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
80 solver->setPolarity(a.
var_no(), value ? l_True : l_False);
82 catch(Minisat::OutOfMemoryException)
84 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
85 status = statust::ERROR;
86 throw std::bad_alloc();
104 return "MiniSAT 2.2.1 without simplifier";
109 return "MiniSAT 2.2.1 with simplifier";
115 while((
unsigned)
solver->nVars()<no_variables())
126 for(
const auto &literal : bv)
128 if(literal.is_true())
130 else if(!literal.is_false())
133 literal.var_no() < (
unsigned)
solver->nVars(),
134 "variable not added yet");
138 Minisat::vec<Minisat::Lit> c;
154 static size_t cnf_clause_index = 0;
156 bool clause_removed = process_clause(bv, cnf);
166 catch(
const Minisat::OutOfMemoryException &)
168 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
169 status = statust::ERROR;
170 throw std::bad_alloc();
186 template <
typename T>
191 log.statistics() << (no_variables() - 1) <<
" variables, "
200 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
202 status = statust::UNSAT;
203 return resultt::P_UNSATISFIABLE;
207 for(
const auto &assumption : assumptions)
209 if(assumption.is_false())
211 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
213 status = statust::UNSAT;
214 return resultt::P_UNSATISFIABLE;
218 Minisat::vec<Minisat::Lit> solver_assumptions;
219 convert(assumptions, solver_assumptions);
221 using Minisat::lbool;
225 void (*old_handler)(int) = SIG_ERR;
227 if(time_limit_seconds != 0)
231 if(old_handler == SIG_ERR)
232 log.warning() <<
"Failed to set solver time limit" <<
messaget::eom;
234 alarm(time_limit_seconds);
237 lbool solver_result =
solver->solveLimited(solver_assumptions);
239 if(old_handler != SIG_ERR)
242 signal(SIGALRM, old_handler);
248 if(time_limit_seconds != 0)
250 log.warning() <<
"Time limit ignored (not supported on Win32 yet)"
254 lbool solver_result =
solver->solve(solver_assumptions) ? l_True : l_False;
258 if(solver_result == l_True)
260 log.status() <<
"SAT checker: instance is SATISFIABLE" <<
messaget::eom;
262 status = statust::SAT;
263 return resultt::P_SATISFIABLE;
266 if(solver_result == l_False)
268 log.status() <<
"SAT checker: instance is UNSATISFIABLE" <<
messaget::eom;
269 status = statust::UNSAT;
270 return resultt::P_UNSATISFIABLE;
273 log.status() <<
"SAT checker: timed out or other error" <<
messaget::eom;
274 status = statust::ERROR;
275 return resultt::P_ERROR;
277 catch(
const Minisat::OutOfMemoryException &)
279 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
280 status=statust::ERROR;
281 return resultt::P_ERROR;
293 bool sign = a.
sign();
296 solver->model.growTo(v + 1);
298 solver->model[v] = Minisat::lbool(value);
300 catch(
const Minisat::OutOfMemoryException &)
302 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
303 status = statust::ERROR;
304 throw std::bad_alloc();
308 template <
typename T>
313 time_limit_seconds(0)
317 template <
typename T>
325 for(
int i=0; i<
solver->conflict.size(); i++)
326 if(var(
solver->conflict[i])==v)
338 for(
const auto &assumption : bv)
340 if(!assumption.is_true())
342 assumptions.push_back(assumption);
360 catch(
const Minisat::OutOfMemoryException &)
364 throw std::bad_alloc();