22#error "Expected HAVE_PICOSAT"
60 for(
const auto &literal : new_bv)
61 picosat_add(
picosat, literal.dimacs());
82 picosat_assume(
picosat, literal.dimacs());
84 const int res=picosat_sat(
picosat, -1);
85 if(res==PICOSAT_SATISFIABLE)
87 msg=
"SAT checker: instance is SATISFIABLE";
95 res == PICOSAT_UNSATISFIABLE,
96 "picosat result should report either sat or unsat");
97 msg=
"SAT checker: instance is UNSATISFIABLE";
102 return P_UNSATISFIABLE;
135 [](
const literalt &l) { return !l.is_constant(); }),
136 "assumptions should be non-constant");
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
@ ERROR
An error occurred during goto checking.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.