10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
27 void lcnf(
const bvt &bv)
override;
bool has_is_in_conflict() const override
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
bool has_set_assumptions() const 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.
CNF Generation, via Tseitin.
std::vector< literalt > bvt
resultt
The result of goto verifying.