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(Minisat::OutOfMemoryException)
148 status = statust::ERROR;
149 throw std::bad_alloc();
171 (no_variables()-1) <<
" variables, " <<
172 solver->nClauses() <<
" clauses" << eom;
182 "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
187 bool has_false=
false;
196 "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
200 Minisat::vec<Minisat::Lit> solver_assumptions;
201 convert(assumptions, solver_assumptions);
203 using Minisat::lbool;
207 void (*old_handler)(int)=SIG_ERR;
209 if(time_limit_seconds!=0)
213 if(old_handler==SIG_ERR)
214 warning() <<
"Failed to set solver time limit" << eom;
216 alarm(time_limit_seconds);
219 lbool solver_result=
solver->solveLimited(solver_assumptions);
221 if(old_handler!=SIG_ERR)
224 signal(SIGALRM, old_handler);
230 if(time_limit_seconds!=0)
233 "Time limit ignored (not supported on Win32 yet)" <<
messaget::eom;
237 solver->solve(solver_assumptions) ? l_True : l_False;
241 if(solver_result==l_True)
244 "SAT checker: instance is SATISFIABLE" << eom;
247 return resultt::P_SATISFIABLE;
249 else if(solver_result==l_False)
252 "SAT checker: instance is UNSATISFIABLE" << eom;
257 "SAT checker: timed out or other error" << eom;
258 status=statust::ERROR;
259 return resultt::P_ERROR;
264 status=statust::UNSAT;
265 return resultt::P_UNSATISFIABLE;
267 catch(Minisat::OutOfMemoryException)
270 "SAT checker ran out of memory" << eom;
271 status=statust::ERROR;
272 return resultt::P_ERROR;
284 bool sign = a.
sign();
287 solver->model.growTo(v + 1);
289 solver->model[v] = Minisat::lbool(value);
291 catch(Minisat::OutOfMemoryException)
294 status = statust::ERROR;
295 throw std::bad_alloc();
301 solver(_solver), time_limit_seconds(0)
322 for(
int i=0; i<
solver->conflict.size(); i++)
323 if(var(
solver->conflict[i])==v)
362 catch(Minisat::OutOfMemoryException)
366 throw std::bad_alloc();
satcheck_minisat_simplifiert()
virtual void lcnf(const bvt &bv) final
virtual const std::string solver_text()
void set_polarity(literalt a, bool value)
virtual const std::string solver_text() final
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
virtual void set_frozen(literalt a) final
#define forall_literals(it, bv)
#define INVARIANT(CONDITION, REASON)
satcheck_minisat_no_simplifiert()
virtual void set_assignment(literalt a, bool value) override
mstreamt & warning() const
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
static Minisat::Solver * solver_to_interrupt
int solver(std::istream &in)
virtual bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
satcheck_minisat2_baset(T *)
#define PRECONDITION(CONDITION)
mstreamt & status() const
bool is_eliminated(literalt a) const
virtual ~satcheck_minisat2_baset()
virtual void set_assumptions(const bvt &_assumptions) override
virtual tvt l_get(literalt a) const final
static void interrupt_solver(int signum)
std::vector< literalt > bvt
virtual resultt prop_solve() override