Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_SMT2_SMT2_DEC_H
11 #define CPROVER_SOLVERS_SMT2_SMT2_DEC_H
34 const std::string &_benchmark,
35 const std::string &_notes,
36 const std::string &_logic,
49 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
Class that provides messages with a built-in verbosity 'level'.
resultt
The result of goto verifying.
std::stringstream stringstream
resultt dec_solve() override
Run the decision procedure to solve the problem.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
resultt read_result(std::istream &in)
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Decision procedure interface for various SMT 2.x solvers.