15 #include <precosat.hh> 18 #error "Expected HAVE_PRECOSAT" 21 #define precosat_lit(a) ((a).var_no()*2 + !(a).sign()) 72 std::to_string(
solver->getAddedOrigClauses())+
" clauses";
78 const int res=
solver->solve();
81 msg=
"SAT checker: instance is SATISFIABLE";
89 msg=
"SAT checker: instance is UNSATISFIABLE";
94 return P_UNSATISFIABLE;
virtual const std::string solver_text()
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
virtual void lcnf(const bvt &bv)
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
PrecoSat::Solver * solver
virtual ~satcheck_precosatt()
virtual resultt prop_solve()
virtual size_t no_variables() const override
std::vector< literalt > bvt