21#include <minisat/core/Solver.h>
22#include <minisat/simp/SimpSolver.h>
25# define l_False Minisat::l_False
26# define l_True Minisat::l_True
30#error "Expected HAVE_MINISAT2"
33void convert(
const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
36 bv.size() <=
static_cast<std::size_t
>(std::numeric_limits<int>::max()));
37 dest.capacity(
static_cast<int>(bv.size()));
39 for(
const auto &literal : bv)
41 if(!literal.is_false())
42 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
49 bv.size() <=
static_cast<std::size_t
>(std::numeric_limits<int>::max()));
50 dest.capacity(
static_cast<int>(bv.size()));
52 for(
const auto &literal : bv)
55 if(!literal.is_true())
56 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
100 catch(Minisat::OutOfMemoryException)
104 throw std::bad_alloc();
122 return "MiniSAT 2.2.1 without simplifier";
127 return "MiniSAT 2.2.1 with simplifier";
144 for(
const auto &literal : bv)
146 if(literal.is_true())
148 else if(!literal.is_false())
151 literal.var_no() < (
unsigned)
solver->nVars(),
152 "variable not added yet");
156 Minisat::vec<Minisat::Lit> c;
173 static size_t cnf_clause_index = 0;
181 bv, cnf, cnf_clause_index, !clause_removed);
186 catch(
const Minisat::OutOfMemoryException &)
190 throw std::bad_alloc();
220 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
227 for(
const auto &assumption : assumptions)
229 if(assumption.is_false())
231 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
238 Minisat::vec<Minisat::Lit> solver_assumptions;
241 using Minisat::lbool;
245 void (*old_handler)(int) = SIG_ERR;
251 if(old_handler == SIG_ERR)
257 lbool solver_result =
solver->solveLimited(solver_assumptions);
259 if(old_handler != SIG_ERR)
262 signal(SIGALRM, old_handler);
270 log.warning() <<
"Time limit ignored (not supported on Win32 yet)"
278 if(solver_result ==
l_True)
297 catch(
const Minisat::OutOfMemoryException &)
313 bool sign = a.
sign();
316 solver->model.growTo(v + 1);
318 solver->model[v] = Minisat::lbool(value);
320 catch(
const Minisat::OutOfMemoryException &)
324 throw std::bad_alloc();
345 for(
int i=0; i<
solver->conflict.size(); i++)
346 if(var(
solver->conflict[i])==v)
365 catch(
const Minisat::OutOfMemoryException &)
369 throw std::bad_alloc();
cnf_solvert(message_handlert &message_handler)
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual size_t no_variables() const override
std::unique_ptr< clause_hardness_collectort > solver_hardness
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
std::unique_ptr< T > solver
~satcheck_minisat2_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
resultt do_prop_solve(const bvt &) override
satcheck_minisat2_baset(message_handlert &message_handler)
void set_polarity(literalt a, bool value)
void lcnf(const bvt &bv) override final
tvt l_get(literalt a) const override final
void set_assignment(literalt a, bool value) override
uint32_t time_limit_seconds
std::string solver_text() const override
void set_frozen(literalt a) override final
bool is_eliminated(literalt a) const
std::string solver_text() const override final
std::vector< literalt > bvt
static Minisat::Solver * solver_to_interrupt
static void interrupt_solver(int signum)
void convert_assumptions(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.