22#error "Expected HAVE_PICOSAT"
87 msg=
"SAT checker: instance is SATISFIABLE";
96 "picosat result should report either sat or unsat");
97 msg=
"SAT checker: instance is UNSATISFIABLE";
135 [](
const literalt &l) { return !l.is_constant(); }),
136 "assumptions should be non-constant");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
mstreamt & statistics() const
mstreamt & status() const
const std::string solver_text() override
resultt do_prop_solve() override
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void lcnf(const bvt &bv) override
std::vector< literalt > bvt
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.