20 #error "Expected HAVE_MINISAT" 25 dest.growTo(bv.size());
27 for(
unsigned i=0; i<bv.size(); i++)
28 dest[i]=Lit(bv[i].var_no(), bv[i].sign());
34 virtual void root(
const vec<Lit> &c)
41 for(
int i=0; i<c.size(); i++)
50 virtual void chain(
const vec<ClauseId> &cs,
const vec<Var> &xs);
61 assert(cs.size()==xs.size()+1);
69 c.
steps.resize(xs.size());
74 for(
int i=0; i<xs.size(); i++)
78 c.
steps[i].clause_id=cs[i+1];
79 c.
steps[i].pivot_var_no=xs[i];
110 return "MiniSAT 1.14p";
138 for(
unsigned i=0; i<new_bv.size(); i++)
139 assert(new_bv[i].var_no()<(unsigned)
solver->nVars());
164 msg=
"empty clause: instance is UNSATISFIABLE";
168 msg=
"SAT checker inconsistent: instance is UNSATISFIABLE";
172 vec<Lit> MiniSat_assumptions;
175 if(
solver->solve(MiniSat_assumptions))
177 msg=
"SAT checker: instance is SATISFIABLE";
180 return P_SATISFIABLE;
183 msg=
"SAT checker: instance is UNSATISFIABLE";
188 return P_UNSATISFIABLE;
195 solver->model.growTo(v+1);
197 solver->model[v]=lbool(value);
204 for(
int i=0; i<
solver->conflict.size(); i++)
206 if(var(
solver->conflict[i])==v)
220 assert(!it->is_constant());
258 return "MiniSAT + Proof";
278 return "MiniSAT + Core";
~satcheck_minisat1_prooft()
virtual void lcnf(const bvt &bv) final
class minisat_prooft * minisat_proof
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
virtual ~minisat_prooft()
virtual void chain(const vec< ClauseId > &cs, const vec< Var > &xs)
satcheck_minisat1_prooft()
virtual resultt prop_solve() override
static mstreamt & eom(mstreamt &m)
simple_prooft resolution_proof
virtual void root(const vec< Lit > &c)
void build_core(std::vector< bool > &in_core)
virtual void deleted(ClauseId c)
virtual tvt l_get(literalt a) const override
virtual ~satcheck_minisat1_baset()
virtual void set_assumptions(const bvt &_assumptions) override
simple_prooft & get_resolution_proof()
~satcheck_minisat1_coret()
satcheck_minisat1_coret()
std::vector< bool > in_core
void convert(const bvt &bv, vec< Lit > &dest)
virtual const std::string solver_text() override
virtual resultt prop_solve() override
virtual size_t no_variables() const override
virtual void set_assignment(literalt a, bool value) override
virtual const std::string solver_text() override
std::vector< literalt > bvt
virtual bool is_in_conflict(literalt l) const override
virtual const std::string solver_text() override