10 #ifndef CPROVER_SOLVERS_SMT2_SMT2_PROP_H 11 #define CPROVER_SOLVERS_SMT2_SMT2_PROP_H 24 const std::string &_benchmark,
25 const std::string &_source,
26 const std::string &_logic,
47 virtual void lcnf(
const bvt &bv);
90 #endif // CPROVER_SOLVERS_SMT2_SMT2_PROP_H virtual void set_no_variables(size_t no)
virtual literalt lselect(literalt a, literalt b, literalt c)
virtual literalt lxor(const bvt &bv)
literalt def_smt2_literal()
virtual literalt land(literalt a, literalt b)
virtual void lcnf(const bvt &bv)
virtual literalt limplies(literalt a, literalt b)
virtual literalt lequal(literalt a, literalt b)
virtual propt::resultt prop_solve()
smt2_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out)
smt2_identifierst smt2_identifiers
std::string smt2_literal(literalt l)
Decision procedure interface for various SMT 2.x solvers.
virtual tvt l_get(literalt literal) const
virtual void reset_assignment()
virtual literalt lor(literalt a, literalt b)
virtual literalt lnand(literalt a, literalt b)
std::set< std::string > smt2_identifierst
virtual const std::string solver_text()
virtual size_t no_variables() const
virtual literalt lnor(literalt a, literalt b)
literalt define_new_variable()
virtual void set_assignment(literalt a, bool value)
std::vector< tvt > assignment
virtual literalt new_variable()
std::vector< literalt > bvt