68 return std::string(ipasir_signature());
77 else if(!it->is_false())
79 "reject out of bound variables");
87 ipasir_add(
solver, it->dimacs());
110 "SAT checker inconsistent: instance is UNSATISFIABLE" <<
eom;
115 bvt::const_iterator it = std::find_if(
assumptions.begin(),
122 "got FALSE as assumption: instance is UNSATISFIABLE" <<
eom;
128 ipasir_assume(
solver, it->dimacs());
131 int solver_state=ipasir_solve(
solver);
135 "SAT checker: instance is SATISFIABLE" <<
eom;
139 else if(20==solver_state)
142 "SAT checker: instance is UNSATISFIABLE" <<
eom;
147 "SAT checker: solving returned without solution" <<
eom;
148 throw "solving inside IPASIR SAT solver has been interrupted";
160 INVARIANT(
false,
"method not supported");
184 bvt::const_iterator it = std::find_if(bv.begin(), bv.end(),
is_true);
185 const bool has_true = it != bv.end();
bool is_true(const literalt &l)
virtual resultt prop_solve() override
virtual bool is_in_conflict(literalt a) const override
virtual void lcnf(const bvt &bv) override final
virtual const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
virtual tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
#define INVARIANT(CONDITION, REASON)
bool is_false(const literalt &l)
virtual void set_assumptions(const bvt &_assumptions) override
int solver(std::istream &in)
virtual ~satcheck_ipasirt() override
virtual void set_assignment(literalt a, bool value) override
mstreamt & result() const
mstreamt & status() const
Glucose::SimpSolver * solver
virtual size_t no_variables() const override
std::vector< literalt > bvt