Go to the documentation of this file.
69 return std::string(ipasir_signature());
78 else if(!it->is_false())
80 "reject out of bound variables");
88 ipasir_add(
solver, it->dimacs());
107 log.
status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
113 bvt::const_iterator it = std::find_if(
assumptions.begin(),
119 log.
status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
126 ipasir_assume(
solver, it->dimacs());
129 int solver_state=ipasir_solve(
solver);
136 else if(20==solver_state)
138 log.
status() <<
"SAT checker: instance is UNSATISFIABLE"
143 log.
status() <<
"SAT checker: solving returned without solution"
146 "solving inside IPASIR SAT solver has been interrupted");
158 INVARIANT(
false,
"method not supported");
182 bvt::const_iterator it = std::find_if(bv.begin(), bv.end(),
is_true);
183 const bool has_true = it != bv.end();
void set_assignment(literalt a, bool value) override
std::vector< literalt > bvt
mstreamt & status() const
Glucose::SimpSolver * solver
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
#define forall_literals(it, bv)
bool is_false(const literalt &l)
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
void lcnf(const bvt &bv) override final
virtual ~satcheck_ipasirt() override
int solver(std::istream &in)
void set_assumptions(const bvt &_assumptions) override
virtual size_t no_variables() const override
bool is_true(const literalt &l)
resultt do_prop_solve() override
mstreamt & statistics() const
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...