3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00

remove a few string copies

This commit is contained in:
Nuno Lopes 2023-12-19 14:34:37 +00:00
parent e5f52e2131
commit fcc7b25c19

View file

@ -377,9 +377,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
symbol _s = to_symbol(s); symbol _s = to_symbol(s);
if (_s.is_numerical()) { if (_s.is_numerical()) {
std::ostringstream buffer; return mk_c(c)->mk_external_string(std::to_string(_s.get_num()));
buffer << _s.get_num();
return mk_c(c)->mk_external_string(buffer.str());
} }
else { else {
return mk_c(c)->mk_external_string(_s.str()); return mk_c(c)->mk_external_string(_s.str());
@ -823,7 +821,7 @@ extern "C" {
param_descrs descrs; param_descrs descrs;
th_rewriter::get_param_descrs(descrs); th_rewriter::get_param_descrs(descrs);
descrs.display(buffer); 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(""); Z3_CATCH_RETURN("");
} }
@ -1031,7 +1029,7 @@ extern "C" {
default: default:
UNREACHABLE(); UNREACHABLE();
} }
return mk_c(c)->mk_external_string(buffer.str()); return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }
@ -1066,7 +1064,7 @@ extern "C" {
pp.add_assumption(to_expr(assumptions[i])); pp.add_assumption(to_expr(assumptions[i]));
} }
pp.display_smt2(buffer, to_expr(formula)); pp.display_smt2(buffer, to_expr(formula));
return mk_c(c)->mk_external_string(buffer.str()); return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN(""); Z3_CATCH_RETURN("");
} }