21 #ifndef HAVE_LINGELING
22 #error "Expected HAVE_LINGELING"
58 for(
const auto &literal : new_bv)
59 lgladd(
solver, literal.dimacs());
81 lglassume(
solver, literal.dimacs());
83 const int res=lglsat(
solver);
88 msg=
"SAT checker: instance is SATISFIABLE";
95 INVARIANT(res == 20,
"result value is either 10 or 20");
96 msg=
"SAT checker: instance is UNSATISFIABLE";
101 return P_UNSATISFIABLE;
128 [](
const literalt &l) { return !l.is_constant(); }),
129 "assumptions should be non-constant");
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual size_t no_variables() const override
mstreamt & statistics() const
mstreamt & status() const
void set_assumptions(const bvt &_assumptions) override
const std::string solver_text() override
void lcnf(const bvt &bv) override
tvt l_get(literalt a) const override
virtual ~satcheck_lingelingt()
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
void set_frozen(literalt a) override
bool is_in_conflict(literalt a) const override
Returns true if an assumed literal is in conflict if the formula is UNSAT.
std::vector< literalt > bvt
@ ERROR
An error occurred during goto checking.
int solver(std::istream &in)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.