From b2d5c24c1df440b653bd6a31955849545a8bf6ad Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 20 Dec 2023 16:55:09 +0000
Subject: [PATCH] remove a few string copies
---
src/api/api_ast.cpp | 6 ++----
src/api/api_ast_map.cpp | 4 ++--
src/api/api_context.cpp | 6 +++---
src/api/api_fpa.cpp | 4 ++--
src/api/api_goal.cpp | 4 ++--
src/api/api_model.cpp | 4 ++--
src/api/api_numeral.cpp | 10 +++++-----
src/api/api_solver.cpp | 16 ++++++++--------
src/ast/ast_pp.h | 4 ++--
src/ast/rewriter/pb_rewriter.cpp | 8 ++------
src/ast/well_sorted.cpp | 3 +--
src/math/lp/numeric_pair.h | 1 -
src/model/model_smt2_pp.cpp | 6 ++----
src/sat/sat_cutset.cpp | 2 +-
src/sat/sat_solver.cpp | 2 +-
src/smt/smt_context_pp.cpp | 4 ++--
src/util/sstream.h | 31 -------------------------------
src/util/zstring.cpp | 4 ++--
18 files changed, 39 insertions(+), 80 deletions(-)
delete mode 100644 src/util/sstream.h
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index dfe47b8b5..424b361f3 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -146,8 +146,7 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
if (!p.has_def(d)) {
- std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
- SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+ SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl");
return;
}
expr_ref abs_body(m);
@@ -168,8 +167,7 @@ extern "C" {
return;
}
if (!pd.get_def()->get_cases().empty()) {
- std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
- SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+ SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " has already been given a definition");
return;
}
diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp
index 5976d0e41..523ba1f59 100644
--- a/src/api/api_ast_map.cpp
+++ b/src/api/api_ast_map.cpp
@@ -160,8 +160,8 @@ extern "C" {
for (; it != end; ++it) {
buffer << "\n (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n " << mk_ismt2_pp(it->m_value, mng, 3) << ")";
}
- 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(nullptr);
}
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 66cd715c9..344224dd3 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -338,12 +338,12 @@ namespace api {
std::ostringstream buffer;
app * a = to_app(n);
buffer << mk_pp(a->get_decl(), m()) << " applied to: ";
- if (a->get_num_args() > 1) buffer << "\n";
+ if (a->get_num_args() > 1) buffer << '\n';
for (unsigned i = 0; i < a->get_num_args(); ++i) {
buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort ";
- buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << "\n";
+ buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << '\n';
}
- auto str = buffer.str();
+ auto str = std::move(buffer).str();
warning_msg("%s", str.c_str());
break;
}
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index aeb075e45..3c350ed18 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -1022,7 +1022,7 @@ extern "C" {
if (mpfm.is_inf(val)) mpqm.set(q, 0);
std::stringstream ss;
mpqm.display_decimal(ss, q, sbits);
- return mk_c(c)->mk_external_string(ss.str());
+ return mk_c(c)->mk_external_string(std::move(ss).str());
Z3_CATCH_RETURN("");
}
@@ -1100,7 +1100,7 @@ extern "C" {
}
std::stringstream ss;
ss << exp;
- return mk_c(c)->mk_external_string(ss.str());
+ return mk_c(c)->mk_external_string(std::move(ss).str());
Z3_CATCH_RETURN("");
}
diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index cfe0974df..cbb67f2a2 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -185,7 +185,7 @@ extern "C" {
std::ostringstream buffer;
to_goal_ref(g)->display(buffer);
// Hack for removing the trailing '\n'
- std::string result = buffer.str();
+ std::string result = std::move(buffer).str();
SASSERT(result.size() > 0);
result.resize(result.size()-1);
return mk_c(c)->mk_external_string(std::move(result));
@@ -203,7 +203,7 @@ extern "C" {
}
to_goal_ref(g)->display_dimacs(buffer, include_names);
// Hack for removing the trailing '\n'
- std::string result = buffer.str();
+ std::string result = std::move(buffer).str();
SASSERT(result.size() > 0);
result.resize(result.size()-1);
return mk_c(c)->mk_external_string(std::move(result));
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 3512b4b05..e449cb0ea 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -432,14 +432,14 @@ extern "C" {
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
model_smt2_pp(buffer, mk_c(c)->m(), *(to_model_ref(m)), 0);
// Hack for removing the trailing '\n'
- result = buffer.str();
+ result = std::move(buffer).str();
if (!result.empty())
result.resize(result.size()-1);
}
else {
model_params p;
model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
- result = buffer.str();
+ result = std::move(buffer).str();
}
return mk_c(c)->mk_external_string(std::move(result));
Z3_CATCH_RETURN(nullptr);
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index ebac4de31..98dceffb7 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -189,7 +189,7 @@ extern "C" {
if (ok && r.is_int() && !r.is_neg()) {
std::stringstream strm;
r.display_bin(strm, r.get_num_bits());
- return mk_c(c)->mk_external_string(strm.str());
+ return mk_c(c)->mk_external_string(std::move(strm).str());
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -237,7 +237,7 @@ extern "C" {
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
std::ostringstream buffer;
fu.fm().display_smt2(buffer, tmp, false);
- return mk_c(c)->mk_external_string(buffer.str());
+ return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -288,21 +288,21 @@ extern "C" {
if (u.is_numeral(e, r) && !r.is_int()) {
std::ostringstream buffer;
r.display_decimal(buffer, precision);
- return mk_c(c)->mk_external_string(buffer.str());
+ return mk_c(c)->mk_external_string(std::move(buffer).str());
}
if (u.is_irrational_algebraic_numeral(e)) {
algebraic_numbers::anum const & n = u.to_irrational_algebraic_numeral(e);
algebraic_numbers::manager & am = u.am();
std::ostringstream buffer;
am.display_decimal(buffer, n, precision);
- return mk_c(c)->mk_external_string(buffer.str());
+ return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm))
return Z3_get_numeral_string(c, a);
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), ftmp)) {
std::ostringstream buffer;
fu.fm().display_decimal(buffer, ftmp, 12);
- return mk_c(c)->mk_external_string(buffer.str());
+ return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else if (Z3_get_numeral_rational(c, a, r)) {
return mk_c(c)->mk_external_string(r.to_string());
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 953167fe9..ac100ee30 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -170,8 +170,8 @@ extern "C" {
if (g_is_threaded || g_thread_id != std::this_thread::get_id()) {
g_is_threaded = true;
std::ostringstream strm;
- strm << smt2log << "-" << std::this_thread::get_id();
- smt2log = symbol(strm.str());
+ strm << smt2log << '-' << std::this_thread::get_id();
+ smt2log = symbol(std::move(strm).str());
}
to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str());
}
@@ -208,7 +208,7 @@ extern "C" {
if (!smt_logics::supported_logic(to_symbol(logic))) {
std::ostringstream strm;
strm << "logic '" << to_symbol(logic) << "' is not recognized";
- SET_ERROR_CODE(Z3_INVALID_ARG, strm.str());
+ SET_ERROR_CODE(Z3_INVALID_ARG, std::move(strm).str());
RETURN_Z3(nullptr);
}
else {
@@ -306,7 +306,7 @@ extern "C" {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
- SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
+ SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(errstrm).str());
return;
}
@@ -333,7 +333,7 @@ extern "C" {
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
if (!parse_dimacs(is, err, solver)) {
- SET_ERROR_CODE(Z3_PARSER_ERROR, err.str());
+ SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(err).str());
return;
}
sat2goal s2g;
@@ -400,7 +400,7 @@ extern "C" {
if (!initialized)
to_solver(s)->m_solver = nullptr;
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("");
}
@@ -799,7 +799,7 @@ extern "C" {
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->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("");
}
@@ -810,7 +810,7 @@ extern "C" {
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->display_dimacs(buffer, include_names);
- 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/ast/ast_pp.h b/src/ast/ast_pp.h
index 7ccb8ec15..1f20ce300 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -58,13 +58,13 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
inline std::string operator+(char const* s, mk_pp const& pp) {
std::ostringstream strm;
strm << s << pp;
- return strm.str();
+ return std::move(strm).str();
}
inline std::string operator+(std::string const& s, mk_pp const& pp) {
std::ostringstream strm;
strm << s << pp;
- return strm.str();
+ return std::move(strm).str();
}
inline std::string& operator+=(std::string& s, mk_pp const& pp) {
diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
index 2f06710ff..4f1fe3fd1 100644
--- a/src/ast/rewriter/pb_rewriter.cpp
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -157,9 +157,7 @@ expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
continue;
}
- std::ostringstream strm;
- strm << 'x' << i;
- name = symbol(strm.str());
+ name = symbol('x' + std::to_string(i));
trail.push_back(m.mk_const(name, a.mk_int()));
expr* x = trail.back();
m.is_not(e,e);
@@ -188,9 +186,7 @@ void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args,
}
void pb_rewriter::dump_pb_rewrite(expr* fml) {
- std::ostringstream strm;
- strm << "pb_rewrite_" << (s_lemma++) << ".smt2";
- std::ofstream out(strm.str());
+ std::ofstream out("pb_rewrite_" + std::to_string(s_lemma++) + ".smt2");
ast_smt_pp pp(m());
pp.display_smt2(out, fml);
out.close();
diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp
index fa8e2768b..84cdf28ad 100644
--- a/src/ast/well_sorted.cpp
+++ b/src/ast/well_sorted.cpp
@@ -70,8 +70,7 @@ struct well_sorted_proc {
strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n';
strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n';
strm << "Function sort: " << mk_pp(decl, m_manager) << '.';
- auto str = strm.str();
- warning_msg("%s", str.c_str());
+ warning_msg("%s", std::move(strm).str().c_str());
m_error = true;
return;
}
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index 251274006..93780f7be 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -24,7 +24,6 @@
#include <algorithm>
#ifdef lp_for_z3
#include "util/rational.h"
-#include "util/sstream.h"
#include "util/z3_exception.h"
#else
// include "util/numerics/mpq.h"
diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp
index b5ac3fbad..89ea98075 100644
--- a/src/model/model_smt2_pp.cpp
+++ b/src/model/model_smt2_pp.cpp
@@ -68,7 +68,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
buffer << " ";
}
buffer << "\n-----------";
- std::string buffer_str = buffer.str();
+ std::string buffer_str = std::move(buffer).str();
unsigned len = static_cast<unsigned>(buffer_str.length());
pp_indent(out, indent);
out << ";; ";
@@ -206,9 +206,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
if (f_i->is_partial()) {
body = mk_string(m, "#unspecified");
for (unsigned j = 0; j < f->get_arity(); j++) {
- std::stringstream strm;
- strm << "x!" << (j+1);
- var_names.push_back(symbol(strm.str()));
+ var_names.push_back(symbol("x!" + std::to_string(j+1)));
}
}
else {
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index aae9bf1ab..2d31bcf14 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -273,7 +273,7 @@ namespace sat {
std::string cut::table2string(unsigned num_input, uint64_t table) {
std::ostringstream strm;
display_table(strm, num_input, table);
- return strm.str();
+ return std::move(strm).str();
}
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a1b88bed1..2d2962940 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2280,7 +2280,7 @@ namespace sat {
<< std::setw(4) << m_stats.m_restart
<< mk_stat(*this)
<< " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
- std::string str(strm.str());
+ std::string str = std::move(strm).str();
svector<size_t> nums;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 3925a4e21..4842f6e23 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -510,7 +510,7 @@ namespace smt {
#else
strm << "lemma_" << (++m_lemma_id) << ".smt2";
#endif
- return strm.str();
+ return std::move(strm).str();
}
@@ -722,7 +722,7 @@ namespace smt {
<< std::setw(4) << m_stats.m_num_del_clauses << " "
<< std::setw(7) << mem_stat() << ")\n";
- std::string str(strm.str());
+ std::string str = std::move(strm).str();
svector<size_t> offsets;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;
diff --git a/src/util/sstream.h b/src/util/sstream.h
deleted file mode 100644
index fba13c5d5..000000000
--- a/src/util/sstream.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
-Copyright (c) 2018 Microsoft Corporation
-
-Module Name:
-
- nat_set.h
-
-Abstract:
-
- Wrapper for sstream.
-
-Author:
-
- Leonardo de Moura (leonardo) 2013
-
-Revision History:
-
-*/
-#pragma once
-#include <sstream>
-#include <string>
-
-namespace lean {
-/** \brief Wrapper for std::ostringstream */
-class sstream {
- std::ostringstream m_strm;
-public:
- std::string str() const { return m_strm.str(); }
- template<typename T> sstream & operator<<(T const & t) { m_strm << t; return *this; }
-};
-}
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index eaa5bb5ee..8e08820f6 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -152,7 +152,7 @@ std::string zstring::encode() const {
unsigned ch = m_buffer[i];
if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) {
_flush();
- strm << "\\u{" << std::hex << ch << std::dec << "}";
+ strm << "\\u{" << std::hex << ch << std::dec << '}';
}
else {
if (offset == 99)
@@ -161,7 +161,7 @@ std::string zstring::encode() const {
}
}
_flush();
- return strm.str();
+ return std::move(strm).str();
}
bool zstring::suffixof(zstring const& other) const {