mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

api: avoid some string copies when using mk_external_string

Browse source
This commit is contained in:
Nuno Lopes 2024-12-28 09:42:54 +00:00
parent 0b9ed925d6
commit bd8c870bbe
11 changed files with 25 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -1799,7 +1799,7 @@ def write_log_h_preamble(log_h):
log_h.write('extern atomic<bool> 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')

15
src/api/api_context.cpp
View file

@ -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<char *>(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<char *>(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<char *>(m_string_buffer.c_str());
return m_string_buffer.c_str();
}
expr * context::mk_numeral_core(rational const & n, sort * s) {

4
src/api/api_context.h
View file

@ -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<char> m_char_buffer;

2
src/api/api_datalog.cpp
View file

@ -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("");
}

2
src/api/api_log.cpp
View file

@ -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';
}

10
src/api/api_numeral.cpp
View file

@ -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;
}
}

2
src/api/api_opt.cpp
View file

@ -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("");
}

2
src/api/api_params.cpp
View file

@ -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);
}

8
src/api/api_parsers.cpp
View file

@ -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()));
}
}

4
src/api/api_rcf.cpp
View file

@ -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("");
}

14
src/api/api_tactic.cpp
View file

@ -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<dependent_expr_simplifier> 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("");
}