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)
31 dest.capacity(bv.size());
35 dest.push(Minisat::mkLit(it->var_no(), it->sign()));
48 if(a.
var_no()>=(unsigned)solver->model.size())
53 if(solver->model[a.
var_no()]==l_True)
55 else if(solver->model[a.
var_no()]==l_False)
71 solver->setPolarity(a.
var_no(), value);
76 return "MiniSAT 2.2.1 without simplifier";
81 return "MiniSAT 2.2.1 with simplifier";
100 else if(!it->is_false())
101 assert(it->var_no()<(unsigned)
solver->nVars());
104 Minisat::vec<Minisat::Lit> c;
134 "SAT checker inconsistent: instance is UNSATISFIABLE" <<
eom;
139 bool has_false=
false;
148 "got FALSE as assumption: instance is UNSATISFIABLE" <<
eom;
152 Minisat::vec<Minisat::Lit> solver_assumptions;
155 if(
solver->solve(solver_assumptions))
158 "SAT checker: instance is SATISFIABLE" <<
eom;
166 "SAT checker: instance is UNSATISFIABLE" <<
eom;
174 catch(Minisat::OutOfMemoryException)
177 "SAT checker ran out of memory" <<
eom;
192 solver->model.growTo(v+1);
194 solver->model[v]=Minisat::lbool(value);
220 for(
int i=0; i<
solver->conflict.size(); i++)
221 if(var(
solver->conflict[i])==v)
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)
satcheck_minisat_no_simplifiert()
virtual void set_assignment(literalt a, bool value) override
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
virtual bool is_in_conflict(literalt a) const override
satcheck_minisat2_baset(T *)
bool is_eliminated(literalt a) const
virtual ~satcheck_minisat2_baset()
virtual void set_assumptions(const bvt &_assumptions) override
virtual size_t no_variables() const override
virtual tvt l_get(literalt a) const final
std::vector< literalt > bvt
virtual resultt prop_solve() override