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,
42 dec_solve_was_called(false)
47 virtual std::string decision_procedure_text()
const;
53 resultt read_result_boolector(std::istream &in);
54 resultt read_result_cvc3(std::istream &in);
55 resultt read_result_opensmt(std::istream &in);
56 resultt read_result_mathsat(std::istream &in);
57 resultt read_result_yices(std::istream &in);
58 resultt read_result_z3(std::istream &in);
60 bool string_to_expr_z3(
62 const std::string &value,
exprt &e)
const;
64 std::string mathsat_value(
const std::string &src);
75 #endif // CPROVER_SOLVERS_SMT1_SMT1_DEC_H The type of an expression.
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
std::map< std::string, std::string > index_value_mapt
Decision procedure interface for various SMT 1.x solvers.
Base class for all expressions.
std::string temp_result_filename
bool dec_solve_was_called