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