21 #error "Expected HAVE_PICOSAT" 60 picosat_add(
picosat, it->dimacs());
81 picosat_assume(
picosat, it->dimacs());
83 const int res=picosat_sat(
picosat, -1);
84 if(res==PICOSAT_SATISFIABLE)
86 msg=
"SAT checker: instance is SATISFIABLE";
93 assert(res==PICOSAT_UNSATISFIABLE);
94 msg=
"SAT checker: instance is UNSATISFIABLE";
99 return P_UNSATISFIABLE;
129 assert(!it->is_constant());
virtual void set_assumptions(const bvt &_assumptions)
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
virtual const std::string solver_text()
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)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual void set_assignment(literalt a, bool value)
std::vector< literalt > bvt