22 #error "Expected HAVE_PICOSAT" 61 picosat_add(
picosat, it->dimacs());
82 picosat_assume(
picosat, it->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");
virtual void set_assumptions(const bvt &_assumptions)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
#define forall_literals(it, bv)
virtual const std::string solver_text()
#define PRECONDITION(CONDITION)
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
mstreamt & result() const
mstreamt & status() const
virtual bool is_in_conflict(literalt a) const
Returns true if an assumption is in the final conflict.
virtual void lcnf(const bvt &bv)
#define UNREACHABLE
This should be used to mark dead code.
virtual void set_assignment(literalt a, bool value)
std::vector< literalt > bvt