22#error "Expected HAVE_PICOSAT"
60 for(
const auto &literal : new_bv)
61 picosat_add(
picosat, literal.dimacs());
75 std::to_string(picosat_added_original_clauses(
picosat))+
" clauses";
81 for(
const auto &literal : assumptions)
82 if(!literal.is_true())
83 picosat_assume(
picosat, literal.dimacs());
85 const int res=picosat_sat(
picosat, -1);
86 if(res==PICOSAT_SATISFIABLE)
88 msg=
"SAT checker: instance is SATISFIABLE";
96 res == PICOSAT_UNSATISFIABLE,
97 "picosat result should report either sat or unsat");
98 msg=
"SAT checker: instance is UNSATISFIABLE";
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
std::string solver_text() const override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
resultt do_prop_solve(const bvt &assumptions) override
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'.