From bd8c870bbee49da9756c1408b3f162897ad74ffa Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 28 Dec 2024 09:42:54 +0000 Subject: [PATCH] api: avoid some string copies when using mk_external_string --- scripts/update_api.py | 2 +- src/api/api_context.cpp | 15 ++------------- src/api/api_context.h | 4 +--- src/api/api_datalog.cpp | 2 +- src/api/api_log.cpp | 2 +- src/api/api_numeral.cpp | 10 +++++----- src/api/api_opt.cpp | 2 +- src/api/api_params.cpp | 2 +- src/api/api_parsers.cpp | 8 +++----- src/api/api_rcf.cpp | 4 ++-- src/api/api_tactic.cpp | 14 +++++++------- 11 files changed, 25 insertions(+), 40 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 79f144142..cbea973b3 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1799,7 +1799,7 @@ def write_log_h_preamble(log_h): log_h.write('extern atomic g_z3_log_enabled;\n') log_h.write('void ctx_enable_logging();\n') log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n') - log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') + log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6f7a424ea..acc4d7016 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -209,21 +209,10 @@ namespace api { invoke_error_handler(err); } } - - char * context::mk_external_string(char const * str) { - m_string_buffer = str?str:""; - return const_cast(m_string_buffer.c_str()); - } - - char * context::mk_external_string(char const * str, unsigned n) { - m_string_buffer.clear(); - m_string_buffer.append(str, n); - return const_cast(m_string_buffer.c_str()); - } - char * context::mk_external_string(std::string && str) { + const char * context::mk_external_string(std::string && str) { m_string_buffer = std::move(str); - return const_cast(m_string_buffer.c_str()); + return m_string_buffer.c_str(); } expr * context::mk_numeral_core(rational const & n, sort * s) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 8b049ce16..2838bcb05 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -199,9 +199,7 @@ namespace api { // Store a copy of str in m_string_buffer, and return a reference to it. // This method is used to communicate local/internal strings with the "external world" - char * mk_external_string(char const * str, unsigned n); - char * mk_external_string(char const * str); - char * mk_external_string(std::string && str); + const char * mk_external_string(std::string && str); sbuffer m_char_buffer; diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 8f436bf8a..3d437e983 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -559,7 +559,7 @@ extern "C" { param_descrs descrs; to_fixedpoint_ref(d)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index ed5f68e8a..e84ece780 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -34,7 +34,7 @@ static mutex g_log_mux; #endif // functions called from api_log_macros.* -void SetR(void * obj) { +void SetR(const void * obj) { *g_z3_log << "= " << obj << '\n'; } diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index b90a84bb7..4e99e05f0 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -217,20 +217,20 @@ extern "C" { if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) { switch (rm) { case MPF_ROUND_NEAREST_TEVEN: - return mk_c(c)->mk_external_string("roundNearestTiesToEven"); + return "roundNearestTiesToEven"; break; case MPF_ROUND_NEAREST_TAWAY: - return mk_c(c)->mk_external_string("roundNearestTiesToAway"); + return "roundNearestTiesToAway"; break; case MPF_ROUND_TOWARD_POSITIVE: - return mk_c(c)->mk_external_string("roundTowardPositive"); + return "roundTowardPositive"; break; case MPF_ROUND_TOWARD_NEGATIVE: - return mk_c(c)->mk_external_string("roundTowardNegative"); + return "roundTowardNegative"; break; case MPF_ROUND_TOWARD_ZERO: default: - return mk_c(c)->mk_external_string("roundTowardZero"); + return "roundTowardZero"; break; } } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 556b1345b..ef215941e 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -313,7 +313,7 @@ extern "C" { param_descrs descrs; to_optimize_ptr(d)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 2d0770903..aa44e56ee 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -191,7 +191,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } - return mk_c(c)->mk_external_string(result); + return result; Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index ae245fbdc..8f6c76958 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -235,9 +235,9 @@ extern "C" { Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) { std::stringstream ous; - Z3_TRY; RESET_ERROR_CODE(); LOG_Z3_eval_smtlib2_string(c, str); + Z3_TRY; if (!mk_c(c)->cmd()) { auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m())); mk_c(c)->cmd() = ctx; @@ -257,15 +257,13 @@ extern "C" { // See api::context::m_parser for a motivation about the reuse of the parser if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) { SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } } catch (z3_exception& e) { if (ous.str().empty()) ous << e.what(); SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); - Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str())); + Z3_CATCH_CORE(); + RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str())); } } diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index ccc79bc46..684e8c617 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -274,7 +274,7 @@ extern "C" { reset_rcf_cancel(c); std::ostringstream buffer; rcfm(c).display(buffer, to_rcnumeral(a), compact, html); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -285,7 +285,7 @@ extern "C" { reset_rcf_cancel(c); std::ostringstream buffer; rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 351b3d1b9..af5696132 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -339,7 +339,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -359,7 +359,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -371,7 +371,7 @@ extern "C" { param_descrs descrs; to_tactic_ref(t)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -499,8 +499,8 @@ extern "C" { for (unsigned i = 0; i < sz; i++) { to_apply_result(r)->m_subgoals[i]->display(buffer); } - buffer << ")"; - return mk_c(c)->mk_external_string(buffer.str()); + buffer << ')'; + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -578,7 +578,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -634,7 +634,7 @@ extern "C" { scoped_ptr simp = (*to_simplifier_ref(t))(m, p, st); simp->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); }