10 #ifndef CPROVER_SOLVERS_SMT1_SMT1_DEC_H 11 #define CPROVER_SOLVERS_SMT1_SMT1_DEC_H 35 const std::string &_benchmark,
36 const std::string &_source,
37 const std::string &_logic,
62 const std::string &value,
exprt &e)
const;
75 #endif // CPROVER_SOLVERS_SMT1_SMT1_DEC_H The type of an expression.
resultt read_result_opensmt(std::istream &in)
index_value_mapt index_value_map
smt1_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver)
std::string temp_out_filename
virtual resultt dec_solve()
resultt read_result_mathsat(std::istream &in)
std::map< std::string, std::string > index_value_mapt
virtual std::string decision_procedure_text() const
resultt read_result_z3(std::istream &in)
resultt read_result_cvc3(std::istream &in)
resultt read_result_boolector(std::istream &in)
read model produced by Boolector
Decision procedure interface for various SMT 1.x solvers.
resultt read_result_yices(std::istream &in)
Base class for all expressions.
bool string_to_expr_z3(const typet &type, const std::string &value, exprt &e) const
std::string temp_result_filename
bool dec_solve_was_called
std::string mathsat_value(const std::string &src)