diff --git a/src/api/api_context.h b/src/api/api_context.h index 7009250cc..185eb9e0f 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -34,6 +34,7 @@ Revision History: #include "util/event_handler.h" #include "cmd_context/tactic_manager.h" #include "cmd_context/context_params.h" +#include "cmd_context/cmd_context.h" #include "api/api_polynomial.h" #include "util/hashtable.h" @@ -53,6 +54,7 @@ namespace api { context_params m_params; bool m_user_ref_count; //!< if true, the user is responsible for managing reference counters. scoped_ptr m_manager; + scoped_ptr m_cmd; add_plugins m_plugins; arith_util m_arith_util; @@ -114,6 +116,7 @@ namespace api { ast_manager & m() const { return *(m_manager.get()); } context_params & params() { return m_params; } + scoped_ptr& cmd() { return m_cmd; } bool produce_proofs() const { return m().proofs_enabled(); } bool produce_models() const { return m_params.m_model; } bool produce_unsat_cores() const { return m_params.m_unsat_core; } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 2e33c1a13..830bef7a8 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -117,4 +117,31 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); } + + Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) { + Z3_TRY; + LOG_Z3_eval_smtlib2_string(c, str); + if (!mk_c(c)->cmd()) { + mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m())); + } + scoped_ptr& ctx = mk_c(c)->cmd(); + std::string s(str); + std::istringstream is(s); + std::stringstream ous; + ctx->set_regular_stream(ous); + try { + if (!parse_smt2_commands(*ctx.get(), is)) { + mk_c(c)->m_parser_error_buffer = ous.str(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + RETURN_Z3(nullptr); + } + } + catch (z3_exception& e) { + mk_c(c)->m_parser_error_buffer = e.msg(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + RETURN_Z3(nullptr); + } + RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); + Z3_CATCH_RETURN(nullptr); + } }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 87bb4d818..50ed85c70 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5209,6 +5209,17 @@ extern "C" { Z3_func_decl const decls[]); + /** + \brief Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next + evaluation builds on top of the previous call. + + \returns output generated from processing commands. + + def_API('Z3_eval_smtlib2_string', STRING, (_in(CONTEXT), _in(STRING),)) + */ + + Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str); + /** \brief Retrieve that last error message information generated from parsing.