64 return std::string(ipasir_signature());
69 for(
const auto &literal : bv)
73 else if(!literal.is_false())
77 "reject out of bound variables");
81 for(
const auto &literal : bv)
83 if(!literal.is_false())
86 ipasir_add(
solver, literal.dimacs());
98 static size_t cnf_clause_index = 0;
119 bvt::const_iterator it =
125 log.
status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
132 if(!literal.is_false())
133 ipasir_assume(
solver, literal.dimacs());
137 int solver_state = ipasir_solve(
solver);
138 if(10 == solver_state)
144 else if(20 == solver_state)
150 log.
status() <<
"SAT checker: solving returned without solution"
153 "solving inside IPASIR SAT solver has been interrupted");
164 INVARIANT(
false,
"method not supported");
188 bvt::const_iterator it = std::find_if(bv.begin(), bv.end(),
is_true);
189 const bool has_true = it != bv.end();
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
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
void set_assumptions(const bvt &_assumptions) override
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
resultt do_prop_solve() override
virtual ~satcheck_ipasirt() override
satcheck_ipasirt(message_handlert &message_handler)
void lcnf(const bvt &bv) override final
void set_assignment(literalt a, bool value) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
bool is_false(const literalt &l)
bool is_true(const literalt &l)
std::vector< literalt > bvt
int solver(std::istream &in)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A structure that facilitates collecting the complexity statistics from a decision procedure.
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.