21#error "Expected HAVE_MINISAT"
26 dest.growTo(bv.size());
28 for(
unsigned i=0;
i<bv.size();
i++)
42 for(
int i=0;
i<
c.size();
i++)
69 c.first_clause_id=
cs[0];
70 c.steps.resize(
xs.size());
75 for(
int i=0;
i<
xs.size();
i++)
79 c.steps[
i].clause_id=
cs[
i+1];
80 c.steps[
i].pivot_var_no=
xs[
i];
93 INVARIANT(
a.var_no() != 0,
"variable number should be set");
95 a.var_no() < (
unsigned)
solver->model.size(),
96 "variable number should be within bounds");
113 return "MiniSAT 1.14p";
145 [](
const literalt &l) { return l.var_no() < (unsigned)solver->nVars(); }),
146 "variable number should be within bounds");
168 msg=
"empty clause: instance is UNSATISFIABLE";
172 msg=
"SAT checker inconsistent: instance is UNSATISFIABLE";
181 msg=
"SAT checker: instance is SATISFIABLE";
187 msg=
"SAT checker: instance is UNSATISFIABLE";
197 unsigned v=
a.var_no();
199 solver->model.growTo(v+1);
208 for(
int i=0;
i<
solver->conflict.size();
i++)
210 if(var(
solver->conflict[
i])==v)
224 INVARIANT(!it->is_constant(),
"assumptions should be non-constant");
262 return "MiniSAT + Proof";
282 return "MiniSAT + Core";
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
mstreamt & statistics() const
mstreamt & status() const
virtual void root(const vec< Lit > &c)
virtual void chain(const vec< ClauseId > &cs, const vec< Var > &xs)
virtual void deleted(ClauseId c)
simple_prooft resolution_proof
virtual ~minisat_prooft()
virtual resultt do_prop_solve()=0
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
resultt do_prop_solve() override
bool is_in_conflict(literalt l) const override
Returns true if an assumption is in the final conflict.
void lcnf(const bvt &bv) final
virtual ~satcheck_minisat1_baset()
tvt l_get(literalt a) const override
void set_assumptions(const bvt &_assumptions) override
resultt do_prop_solve() override
satcheck_minisat1_coret()
~satcheck_minisat1_coret()
std::vector< bool > in_core
const std::string solver_text() override
const std::string solver_text() override
~satcheck_minisat1_prooft()
class minisat_prooft * minisat_proof
satcheck_minisat1_prooft()
simple_prooft & get_resolution_proof()
std::vector< literalt > bvt
void convert(const bvt &bv, vec< Lit > &dest)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.