20 #ifndef HAVE_LINGELING 21 #error "Expected HAVE_LINGELING" 58 lgladd(
solver, it->dimacs());
80 lglassume(
solver, it->dimacs());
82 const int res=lglsat(
solver);
85 msg=
"SAT checker: instance is SATISFIABLE";
93 msg=
"SAT checker: instance is UNSATISFIABLE";
98 return P_UNSATISFIABLE;
122 assert(!it->is_constant());
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_frozen(literalt a)
virtual resultt prop_solve()
int solver(std::istream &in)
virtual const std::string solver_text()
virtual void set_assumptions(const bvt &_assumptions)
virtual bool is_in_conflict(literalt a) const
Returns true if an assumed literal is in conflict if the formula is UNSAT.
mstreamt & result() const
mstreamt & status() const
virtual ~satcheck_lingelingt()
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
virtual size_t no_variables() const override
std::vector< literalt > bvt