10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_GLUCOSE_H 11 #define CPROVER_SOLVERS_SAT_SATCHECK_GLUCOSE_H 36 virtual void lcnf(
const bvt &bv);
37 virtual void set_assignment(
literalt a,
bool value);
40 virtual void set_assumptions(
const bvt &_assumptions);
43 void set_polarity(
literalt a,
bool value);
45 virtual bool is_in_conflict(
literalt a)
const;
61 virtual const std::string solver_text();
69 virtual const std::string solver_text();
71 bool is_eliminated(
literalt a)
const;
74 #endif // CPROVER_SOLVERS_SAT_SATCHECK_GLUCOSE_H CNF Generation, via Tseitin.
virtual bool has_set_assumptions() const
virtual bool has_is_in_conflict() const
std::vector< literalt > bvt