10 #ifndef CPROVER_SOLVERS_SMT2_SMT2_DEC_H 11 #define CPROVER_SOLVERS_SMT2_SMT2_DEC_H 30 const std::string &_benchmark,
31 const std::string &_notes,
32 const std::string &_logic,
48 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
std::stringstream stringstream
resultt read_result(std::istream &in)
virtual resultt dec_solve()
Decision procedure interface for various SMT 2.x solvers.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual std::string decision_procedure_text() const
virtual bool has_set_assumptions() const
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)