10 #ifndef CPROVER_SOLVERS_SMT1_SMT1_PROP_H 11 #define CPROVER_SOLVERS_SMT1_SMT1_PROP_H 23 const std::string &_benchmark,
24 const std::string &_source,
25 const std::string &_logic,
45 virtual void lcnf(
const bvt &bv);
81 #endif // CPROVER_SOLVERS_SMT1_SMT1_PROP_H std::vector< tvt > assignment
virtual void reset_assignment()
virtual literalt lnor(literalt a, literalt b)
virtual void lcnf(const bvt &bv)
virtual literalt land(literalt a, literalt b)
virtual size_t no_variables() const
virtual literalt lxor(const bvt &bv)
virtual literalt new_variable()
std::string smt1_literal(literalt l)
virtual literalt lor(literalt a, literalt b)
virtual literalt limplies(literalt a, literalt b)
virtual literalt lselect(literalt a, literalt b, literalt c)
Decision procedure interface for various SMT 1.x solvers.
literalt def_smt1_literal()
virtual void set_assignment(literalt a, bool value)
virtual literalt lequal(literalt a, literalt b)
virtual literalt lnand(literalt a, literalt b)
virtual const std::string solver_text()
virtual propt::resultt prop_solve()
virtual void set_no_variables(size_t no)
smt1_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, std::ostream &_out)
std::vector< literalt > bvt
virtual tvt l_get(literalt literal) const