From 23e6adcad36358e8f263d149e5b86d630e6e9555 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 11 Jul 2020 20:24:45 +0100 Subject: [PATCH] fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string --- src/api/api_bv.cpp | 3 +- src/api/api_datalog.cpp | 6 +- src/api/api_numeral.cpp | 2 +- src/api/api_params.cpp | 12 ++-- src/api/c++/z3++.h | 17 ++--- src/ast/ast.h | 2 + src/ast/ast_smt2_pp.cpp | 67 +++++++++---------- src/ast/ast_smt_pp.cpp | 4 +- src/ast/format.h | 8 +++ src/ast/macros/quasi_macros.cpp | 4 +- src/ast/pattern/pattern_inference.cpp | 15 +++-- src/ast/rewriter/bv_elim.cpp | 6 +- src/ast/rewriter/pb_rewriter.cpp | 6 +- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/ast/seq_decl_plugin.cpp | 14 ++-- src/ast/seq_decl_plugin.h | 4 +- src/ast/well_sorted.cpp | 9 +-- src/cmd_context/basic_cmds.cpp | 4 +- src/cmd_context/check_logic.cpp | 7 +- src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/parametric_cmd.cpp | 4 +- src/cmd_context/pdecl.cpp | 12 ++-- src/cmd_context/tactic_cmds.cpp | 7 +- src/model/model2expr.cpp | 2 +- src/model/model_smt2_pp.cpp | 6 +- src/model/seq_factory.h | 2 +- src/muz/base/dl_context.cpp | 8 +-- src/muz/base/dl_rule.cpp | 2 +- src/muz/base/hnf.cpp | 3 +- src/muz/bmc/dl_bmc_engine.cpp | 46 ++++++------- src/muz/rel/check_relation.cpp | 10 +-- src/muz/rel/dl_base.cpp | 3 +- src/muz/rel/dl_lazy_table.cpp | 2 +- src/muz/spacer/spacer_context.cpp | 11 +-- src/muz/spacer/spacer_manager.cpp | 2 +- src/muz/spacer/spacer_prop_solver.cpp | 3 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 2 +- .../transforms/dl_mk_unbound_compressor.cpp | 2 +- src/nlsat/tactic/goal2nlsat.cpp | 2 +- src/opt/maxsmt.cpp | 3 +- src/opt/opt_context.cpp | 21 +++--- src/opt/opt_solver.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 7 +- src/parsers/util/pattern_validation.cpp | 3 +- src/qe/qe_arrays.cpp | 2 +- src/qe/qe_datatypes.cpp | 3 +- src/sat/sat_drat.cpp | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 9 ++- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_seq.cpp | 2 +- src/smt/theory_str.cpp | 23 ++----- src/smt/theory_str.h | 5 +- src/smt/theory_str_mc.cpp | 19 +----- src/smt/theory_utvpi_def.h | 7 +- src/solver/solver_pool.cpp | 2 +- src/test/expr_rand.cpp | 4 +- src/test/hilbert_basis.cpp | 2 +- src/test/pb2bv.cpp | 6 +- src/test/qe_arith.cpp | 2 +- src/test/theory_pb.cpp | 2 +- src/util/string_buffer.h | 16 +++++ src/util/symbol.h | 6 +- src/util/util.h | 2 + 64 files changed, 248 insertions(+), 229 deletions(-) diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 7f0888d45..685463e19 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -117,7 +117,8 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_sort s = Z3_get_sort(c, n); unsigned sz = Z3_get_bv_sort_size(c, s); rational max_bound = power(rational(2), sz); - Z3_ast bound = Z3_mk_numeral(c, max_bound.to_string().c_str(), int_s); + auto str = max_bound.to_string(); + Z3_ast bound = Z3_mk_numeral(c, str.c_str(), int_s); Z3_inc_ref(c, bound); Z3_ast zero = Z3_mk_int(c, 0, s); Z3_inc_ref(c, zero); diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 4b29a66d6..6bf5af0e6 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -677,9 +677,11 @@ extern "C" { to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); for (unsigned i = 0; i < names.size(); ++i) { - ss << ";" << names[i].str(); + if (i != 0) + ss << ';'; + ss << names[i].str(); } - return of_symbol(symbol(ss.str().substr(1).c_str())); + return of_symbol(symbol(ss.str())); Z3_CATCH_RETURN(of_symbol(symbol::null)); } diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index a1397a55f..7e655c9d1 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -191,7 +191,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().c_str()); + return mk_c(c)->mk_external_string(strm.str()); } else { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 4d10eff8a..866687b7e 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -66,7 +66,8 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_bool(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v); + auto name = norm_param_name(to_symbol(k)); + to_params(p)->m_params.set_bool(name.c_str(), v); Z3_CATCH; } @@ -77,7 +78,8 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_uint(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_uint(norm_param_name(to_symbol(k)).c_str(), v); + auto name = norm_param_name(to_symbol(k)); + to_params(p)->m_params.set_uint(name.c_str(), v); Z3_CATCH; } @@ -88,7 +90,8 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_double(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_double(norm_param_name(to_symbol(k)).c_str(), v); + auto name = norm_param_name(to_symbol(k)); + to_params(p)->m_params.set_double(name.c_str(), v); Z3_CATCH; } @@ -99,7 +102,8 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_symbol(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_sym(norm_param_name(to_symbol(k)).c_str(), to_symbol(v)); + auto name = norm_param_name(to_symbol(k)); + to_params(p)->m_params.set_sym(name.c_str(), to_symbol(v)); Z3_CATCH; } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a64a546a8..a5e856142 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -74,7 +74,7 @@ namespace z3 { inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); } inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); } - inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); } + inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); } inline void reset_params() { Z3_global_param_reset_all(); } /** @@ -122,9 +122,8 @@ namespace z3 { \brief Set global parameter \c param with integer \c value. */ void set(char const * param, int value) { - std::ostringstream oss; - oss << value; - Z3_set_param_value(m_cfg, param, oss.str().c_str()); + auto str = std::to_string(value); + Z3_set_param_value(m_cfg, param, str.c_str()); } }; @@ -211,9 +210,8 @@ namespace z3 { \brief Update global parameter \c param with Integer \c value. */ void set(char const * param, int value) { - std::ostringstream oss; - oss << value; - Z3_update_param_value(m_ctx, param, oss.str().c_str()); + auto str = std::to_string(value); + Z3_update_param_value(m_ctx, param, str.c_str()); } /** @@ -2839,9 +2837,8 @@ namespace z3 { } handle add(expr const& e, unsigned weight) { assert(e.is_bool()); - std::stringstream strm; - strm << weight; - return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0)); + auto str = std::to_string(weight); + return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0)); } void add(expr const& e, expr const& t) { assert(e.is_bool()); diff --git a/src/ast/ast.h b/src/ast/ast.h index 22f627fb1..6e72a3fa3 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -126,6 +126,7 @@ public: explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {} explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {} + explicit parameter(const std::string &s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -984,6 +985,7 @@ struct builtin_name { decl_kind m_kind; symbol m_name; builtin_name(char const * name, decl_kind k) : m_kind(k), m_name(name) {} + builtin_name(const std::string &name, decl_kind k) : m_kind(k), m_name(name) {} }; /** diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index f040bf47e..4ef42d62c 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -36,12 +36,12 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo if (is_smt2_quoted_symbol(s)) { std::string str = mk_smt2_quoted_symbol(s); len = static_cast(str.length()); - return mk_string(m, str.c_str()); + return mk_string(m, str); } else if (s.is_numerical()) { std::string str = s.str(); len = static_cast(str.length()); - return mk_string(m, str.c_str()); + return mk_string(m, str); } else if (!s.bare_str()) { len = 4; @@ -114,7 +114,7 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) { fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int())); else if (f->get_parameter(i).is_rational()) { std::string str = f->get_parameter(i).get_rational().to_string(); - fs.push_back(mk_string(get_manager(), str.c_str())); + fs.push_back(mk_string(get_manager(), str)); } else fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast()))); @@ -177,7 +177,7 @@ format * smt2_pp_environment::pp_bv_literal(app * t, bool use_bv_lits, bool bv_n format * vf; if (!use_bv_lits) { string_buffer<> buf; - buf << "(_ bv" << val.to_string().c_str() << " " << bv_size << ")"; + buf << "(_ bv" << val.to_string() << ' ' << bv_size << ')'; vf = mk_string(get_manager(), buf.c_str()); } else { @@ -238,30 +238,30 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u string_buffer<> buf; VERIFY(get_futil().is_numeral(t, v)); if (fm.is_nan(v)) { - buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; + buf << "(_ NaN " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ')'; return mk_string(m, buf.c_str()); } else if (fm.is_pinf(v)) { - buf << "(_ +oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; + buf << "(_ +oo " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ')'; return mk_string(m, buf.c_str()); } else if (fm.is_ninf(v)) { - buf << "(_ -oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; + buf << "(_ -oo " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ')'; return mk_string(m, buf.c_str()); } else if (fm.is_pzero(v)) { - buf << "(_ +zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; + buf << "(_ +zero " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ')'; return mk_string(m, buf.c_str()); } else if (fm.is_nzero(v)) { - buf << "(_ -zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; + buf << "(_ -zero " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ')'; return mk_string(m, buf.c_str()); } else if (use_float_real_lits) { - buf << "((_ to_fp " << v.get().get_ebits() << " " << + buf << "((_ to_fp " << v.get().get_ebits() << ' ' << v.get().get_sbits() << ") RTZ " << - fm.to_string(v).c_str() << ")"; + fm.to_string(v) << ')'; return mk_string(m, buf.c_str()); } else { @@ -301,9 +301,8 @@ format * smt2_pp_environment::mk_neg(format * f) const { format * smt2_pp_environment::mk_float(rational const & val) const { SASSERT(val.is_nonneg()); SASSERT(val.is_int()); - std::string s = val.to_string(); - s += ".0"; - return mk_string(get_manager(), s.c_str()); + std::string s = val.to_string() + ".0"; + return mk_string(get_manager(), s); } format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned decimal_prec) { @@ -314,11 +313,11 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d if (u.is_numeral(t, val, is_int)) { if (is_int) { if (val.is_nonneg()) { - return mk_string(get_manager(), val.to_string().c_str()); + return mk_string(get_manager(), val.to_string()); } else { val.neg(); - return mk_neg(mk_string(get_manager(), val.to_string().c_str())); + return mk_neg(mk_string(get_manager(), val.to_string())); } } else { @@ -332,7 +331,7 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d else if (decimal) { std::ostringstream buffer; val.display_decimal(buffer, decimal_prec); - vf = mk_string(get_manager(), buffer.str().c_str()); + vf = mk_string(get_manager(), buffer.str()); } else { format * buffer[2] = { mk_float(numerator(val)), mk_float(denominator(val)) }; @@ -360,7 +359,7 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d else { am.display_root_smt2(buffer, val2); } - vf = mk_string(get_manager(), buffer.str().c_str()); + vf = mk_string(get_manager(), buffer.str()); return is_neg ? mk_neg(vf) : vf; } } @@ -380,16 +379,14 @@ format * smt2_pp_environment::pp_string_literal(app * t) { buffer << encs[i]; } } - buffer << "\""; - return mk_string(get_manager(), buffer.str().c_str()); + buffer << '"'; + return mk_string(get_manager(), buffer.str()); } format * smt2_pp_environment::pp_datalog_literal(app * t) { uint64_t v; VERIFY (get_dlutil().is_numeral(t, v)); - std::ostringstream buffer; - buffer << v; - return mk_string(get_manager(), buffer.str().c_str()); + return mk_string(get_manager(), std::to_string(v)); } format_ns::format * smt2_pp_environment::pp_sort(sort * s) { @@ -440,10 +437,10 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { for (unsigned i = 0; i < sz; i++) { fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i))); } - return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str()); + return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str()); } } - return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); + return format_ns::mk_string(get_manager(), s->get_name().str()); } typedef app_ref_vector format_ref_vector; @@ -557,9 +554,7 @@ class smt2_printer { symbol ensure_quote_sym(symbol const& s) { if (is_smt2_quoted_symbol(s)) { - std::string str; - str = mk_smt2_quoted_symbol(s); - return symbol(str.c_str()); + return symbol(mk_smt2_quoted_symbol(s)); } else return s; @@ -576,7 +571,7 @@ class smt2_printer { else { vname = s.str(); } - f = mk_string(m(), vname.c_str ()); + f = mk_string(m(), vname); } else { // fallback... it is not supposed to happen when the printer is correctly used. @@ -584,7 +579,7 @@ class smt2_printer { buf.append("(:var "); buf.append(v->get_idx()); //buf.append(" "); - //buf.append(v->get_sort()->get_name().str().c_str()); + //buf.append(v->get_sort()->get_name().str()); buf.append(")"); f = mk_string(m(), buf.c_str()); } @@ -604,7 +599,7 @@ class smt2_printer { format * pp_simple_attribute(char const * attr, symbol const & s) { std::string str = ensure_quote(s); - return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str())); + return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str)); } format * pp_labels(bool is_pos, buffer const & names, format * f) { @@ -654,7 +649,7 @@ class smt2_printer { if (m_expr2alias->find(t, idx)) { unsigned lvl = m_aliased_lvls_names[idx].first; symbol const & s = m_aliased_lvls_names[idx].second; - m_format_stack.push_back(mk_string(m(), s.str().c_str())); + m_format_stack.push_back(mk_string(m(), s.str())); m_info_stack.push_back(info(lvl+1, 1, 1)); return true; } @@ -707,7 +702,7 @@ class smt2_printer { << ", lvl: " << f_info.m_lvl << " t: #" << t->get_id() << "\n" << mk_ll_pp(t, m()) << ", is-shared: " << m_soccs.is_shared(t) << "\n";); register_alias(t, f, f_info.m_lvl, a); - m_format_stack.push_back(mk_string(m(), a.str().c_str())); + m_format_stack.push_back(mk_string(m(), a.str())); m_info_stack.push_back(info(f_info.m_lvl + 1, 1, 1)); } else { @@ -811,7 +806,7 @@ class smt2_printer { format * f_def[1] = { m_aliased_pps.get(i) }; decls.reserve(lvl+1); ptr_vector & lvl_decls = decls[lvl]; - lvl_decls.push_back(mk_seq1(m(), f_def, f_def+1, f2f(), f_name.str().c_str())); + lvl_decls.push_back(mk_seq1(m(), f_def, f_def+1, f2f(), f_name.str())); } TRACE("pp_let", tout << "decls.size(): " << decls.size() << "\n";); ptr_buffer buf; @@ -919,9 +914,9 @@ class smt2_printer { var_name = mk_smt2_quoted_symbol (*it); } else { - var_name = it->str (); + var_name = it->str(); } - buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name.c_str ())); + buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name)); } return mk_seq5(m(), buf.begin(), buf.end(), f2f()); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 4524b7f15..1984474a9 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -62,7 +62,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) { if (s.is_numerical()) { buffer << s << k; - return symbol(buffer.str().c_str()); + return symbol(buffer.str()); } if (!s.bare_str()) { @@ -78,7 +78,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) { buffer << "!" << k; } - return symbol(buffer.str().c_str()); + return symbol(buffer.str()); } bool smt_renaming::is_legal(char c) { diff --git a/src/ast/format.h b/src/ast/format.h index abe8b1cee..edbf269f9 100644 --- a/src/ast/format.h +++ b/src/ast/format.h @@ -17,6 +17,7 @@ Revision History: --*/ #pragma once +#include #include "ast/ast.h" @@ -53,6 +54,7 @@ namespace format_ns { family_id get_format_family_id(ast_manager & m); format * mk_string(ast_manager & m, char const * str); + static inline format * mk_string(ast_manager & m, const std::string & str) { return mk_string(m, str.c_str()); } format * mk_int(ast_manager & m, int i); format * mk_unsigned(ast_manager & m, unsigned u); format * mk_indent(ast_manager & m, unsigned i, format * f); @@ -104,6 +106,12 @@ namespace format_ns { mk_string(m, rp))))); } + template + static inline format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, const std::string &header, + char const * lp = "(", char const * rp = ")") { + return mk_seq1(m, begin, end, proc, header.c_str(), lp, rp); + } + #define FORMAT_DEFAULT_INDENT 2 /** diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index fece5e404..3a22758c7 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -206,8 +206,8 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant if (!is_var(arg) || v_seen.get(to_var(arg)->get_idx())) { unsigned inx = m_new_var_names.size(); m_new_name.str(""); - m_new_name << "X" << inx; - m_new_var_names.push_back(symbol(m_new_name.str().c_str())); + m_new_name << 'X' << inx; + m_new_var_names.push_back(symbol(m_new_name.str())); m_new_qsorts.push_back(f->get_domain()[i]); m_new_vars.push_back(m.mk_var(inx + q->get_num_decls(), f->get_domain()[i])); diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 93b269f87..1cc9cfe52 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -631,7 +631,8 @@ bool pattern_inference_cfg::reduce_quantifier( if (new_patterns.empty()) { mk_patterns(q->get_num_decls(), new_body, 0, nullptr, new_patterns); if (m_params.m_pi_warnings && !new_patterns.empty()) { - warning_msg("ignoring nopats annotation because Z3 couldn't find any other pattern (quantifier id: %s)", q->get_qid().str().c_str()); + auto str = q->get_qid().str(); + warning_msg("ignoring nopats annotation because Z3 couldn't find any other pattern (quantifier id: %s)", str.c_str()); } } } @@ -644,8 +645,9 @@ bool pattern_inference_cfg::reduce_quantifier( if (!new_patterns.empty()) { weight = std::max(weight, static_cast(m_params.m_pi_arith_weight)); if (m_params.m_pi_warnings) { + auto str = q->get_qid().str(); warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=).", - q->get_qid().str().c_str(), weight); + str.c_str(), weight); } } } @@ -659,8 +661,9 @@ bool pattern_inference_cfg::reduce_quantifier( if (!new_patterns.empty()) { weight = std::max(weight, static_cast(m_params.m_pi_non_nested_arith_weight)); if (m_params.m_pi_warnings) { + auto str = q->get_qid().str(); warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=).", - q->get_qid().str().c_str(), weight); + str.c_str(), weight); } // verbose_stream() << mk_pp(q, m) << "\n"; } @@ -686,7 +689,8 @@ bool pattern_inference_cfg::reduce_quantifier( mk_patterns(result2->get_num_decls(), result2->get_expr(), 0, nullptr, new_patterns); if (!new_patterns.empty()) { if (m_params.m_pi_warnings) { - warning_msg("pulled nested quantifier to be able to find an usable pattern (quantifier id: %s)", q->get_qid().str().c_str()); + auto str = q->get_qid().str(); + warning_msg("pulled nested quantifier to be able to find an usable pattern (quantifier id: %s)", str.c_str()); } new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr()); if (m.proofs_enabled()) { @@ -699,7 +703,8 @@ bool pattern_inference_cfg::reduce_quantifier( if (new_patterns.empty()) { if (m_params.m_pi_warnings) { - warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", q->get_qid().str().c_str()); + auto str = q->get_qid().str(); + warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", str.c_str()); } TRACE("pi_failed", tout << mk_pp(q, m) << "\n";); } diff --git a/src/ast/rewriter/bv_elim.cpp b/src/ast/rewriter/bv_elim.cpp index f5690b680..898bc39f2 100644 --- a/src/ast/rewriter/bv_elim.cpp +++ b/src/ast/rewriter/bv_elim.cpp @@ -51,12 +51,12 @@ bool bv_elim_cfg::reduce_quantifier(quantifier * q, for (unsigned j = 0; j < num_bits; ++j) { std::ostringstream new_name; new_name << nm.str(); - new_name << "_"; + new_name << '_'; new_name << j; - var* v = m.mk_var(var_idx++, m.mk_bool_sort()); + var* v = m.mk_var(var_idx++, m.mk_bool_sort()); args.push_back(v); _sorts.push_back(m.mk_bool_sort()); - _names.push_back(symbol(new_name.str().c_str())); + _names.push_back(symbol(new_name.str())); } bv = m.mk_app(bfid, OP_MKBV, 0, nullptr, args.size(), args.c_ptr()); _subst_map.push_back(bv.get()); diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 2e2c28edc..d24c38e10 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -158,8 +158,8 @@ expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) { } std::ostringstream strm; - strm << "x" << i; - name = symbol(strm.str().c_str()); + strm << 'x' << i; + name = symbol(strm.str()); trail.push_back(m.mk_const(name, a.mk_int())); expr* x = trail.back(); m.is_not(e,e); @@ -190,7 +190,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().c_str()); + std::ofstream out(strm.str()); ast_smt_pp pp(m()); pp.display_smt2(out, fml); out.close(); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0bec7b7ef..446195896 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1916,7 +1916,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { if (r.is_int() && !r.is_neg()) { - result = str().mk_string(symbol(r.to_string().c_str())); + result = str().mk_string(symbol(r.to_string())); } else { result = str().mk_string(symbol("")); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f862125e0..b2c24547a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -199,12 +199,6 @@ zstring::zstring(unsigned ch) { m_buffer.push_back(ch); } -zstring& zstring::operator=(zstring const& other) { - m_buffer.reset(); - m_buffer.append(other.m_buffer); - return *this; -} - zstring zstring::reverse() const { zstring result; for (unsigned i = length(); i-- > 0; ) { @@ -876,7 +870,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (!(num_parameters == 1 && parameters[0].is_int())) m.raise_exception("character literal expects integer parameter"); zstring zs(parameters[0].get_int()); - parameter p(zs.encode().c_str()); + parameter p(zs.encode()); return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p)); } @@ -991,7 +985,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons init(); for (unsigned i = 0; i < m_sigs.size(); ++i) { if (m_sigs[i]) { - op_names.push_back(builtin_name(m_sigs[i]->m_name.str().c_str(), i)); + op_names.push_back(builtin_name(m_sigs[i]->m_name.str(), i)); } } op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP)); @@ -1024,7 +1018,7 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol app* seq_decl_plugin::mk_string(symbol const& s) { zstring canonStr(s.bare_str()); - symbol canonSym(canonStr.encode().c_str()); + symbol canonSym(canonStr.encode()); parameter param(canonSym); func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); @@ -1032,7 +1026,7 @@ app* seq_decl_plugin::mk_string(symbol const& s) { } app* seq_decl_plugin::mk_string(zstring const& s) { - symbol sym(s.encode().c_str()); + symbol sym(s.encode()); parameter param(sym); func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 58cf04cf7..6edfc2007 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -24,6 +24,7 @@ Revision History: #include "ast/ast.h" #include "ast/bv_decl_plugin.h" +#include #define Z3_USE_UNICODE 0 @@ -121,11 +122,10 @@ public: static unsigned max_char() { return 196607; } zstring() {} zstring(char const* s); + zstring(const std::string &str) : zstring(str.c_str()) {} zstring(unsigned sz, unsigned const* s) { m_buffer.append(sz, s); SASSERT(well_formed()); } - zstring(zstring const& other): m_buffer(other.m_buffer) {} zstring(unsigned num_bits, bool const* ch); zstring(unsigned ch); - zstring& operator=(zstring const& other); zstring replace(zstring const& src, zstring const& dst) const; zstring reverse() const; std::string encode() const; diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp index 0516989e0..ec1551637 100644 --- a/src/ast/well_sorted.cpp +++ b/src/ast/well_sorted.cpp @@ -67,10 +67,11 @@ struct well_sorted_proc { ); std::ostringstream strm; strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m_manager, false) << "\n"; - 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) << "."; - warning_msg("%s", strm.str().c_str()); + 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()); m_error = true; return; } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 3ce523b02..fd9811a01 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -292,7 +292,7 @@ UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", C ctx.print_success(); else { std::string msg = "ignoring unsupported logic " + arg.str(); - ctx.print_unsupported(symbol(msg.c_str()), m_line, m_pos); + ctx.print_unsupported(symbol(msg), m_line, m_pos); } ); @@ -682,7 +682,7 @@ public: ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl; } else if (opt == m_reason_unknown) { - ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown().c_str()) << "\")" << std::endl; + ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown()) << "\")" << std::endl; } else if (opt == m_rlimit) { ctx.regular_stream() << "(:rlimit " << ctx.m().limit().count() << ")" << std::endl; diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 697f8b750..f3c9176e3 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -215,6 +215,11 @@ struct check_logic::imp { struct failed {}; std::string m_last_error; + void fail(std::string &&msg) { + m_last_error = std::move(msg); + throw failed(); + } + void fail(char const * msg) { m_last_error = msg; throw failed(); @@ -473,7 +478,7 @@ struct check_logic::imp { else { std::stringstream strm; strm << "logic does not support theory " << m.get_family_name(fid); - fail(strm.str().c_str()); + fail(strm.str()); } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3cd5504fe..85058cfa8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1656,7 +1656,7 @@ void cmd_context::display_model(model_ref& mdl) { if (p.v1() || p.v2()) { std::ostringstream buffer; model_v2_pp(buffer, *mdl, false); - regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl; + regular_stream() << '"' << escaped(buffer.str(), true) << '"' << std::endl; } else { regular_stream() << "(model " << std::endl; model_smt2_pp(regular_stream(), *this, *mdl, 2); diff --git a/src/cmd_context/parametric_cmd.cpp b/src/cmd_context/parametric_cmd.cpp index 524662ed3..dbbbd556a 100644 --- a/src/cmd_context/parametric_cmd.cpp +++ b/src/cmd_context/parametric_cmd.cpp @@ -26,7 +26,7 @@ char const * parametric_cmd::get_descr(cmd_context & ctx) const { m_descr->append("\nThe following options are available:\n"); std::ostringstream buf; pdescrs(ctx).display(buf, 2); - m_descr->append(buf.str().c_str()); + m_descr->append(buf.str()); } return m_descr->c_str(); } @@ -38,7 +38,7 @@ cmd_arg_kind parametric_cmd::next_arg_kind(cmd_context & ctx) const { void parametric_cmd::set_next_arg(cmd_context & ctx, symbol const & s) { if (m_last == symbol::null) { - m_last = symbol(norm_param_name(s).c_str()); + m_last = symbol(norm_param_name(s)); if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID) throw cmd_exception("invalid keyword argument"); return; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 6aab2390b..fb5b7b9f5 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -808,13 +808,13 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { format * pp(pdecl_manager const & m) const override { if (m_args.empty()) { - return mk_string(m.m(), m_decl->get_name().str().c_str()); + return mk_string(m.m(), m_decl->get_name().str()); } else { ptr_buffer b; for (auto arg : m_args) b.push_back(m.pp(arg)); - return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str()); + return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str()); } } }; @@ -846,11 +846,11 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { format * pp(pdecl_manager const & m) const override { if (m_indices.empty()) { - return mk_string(m.m(), m_decl->get_name().str().c_str()); + return mk_string(m.m(), m_decl->get_name().str()); } else { ptr_buffer b; - b.push_back(mk_string(m.m(), m_decl->get_name().str().c_str())); + b.push_back(mk_string(m.m(), m_decl->get_name().str())); for (auto idx : m_indices) b.push_back(mk_unsigned(m.m(), idx)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_"); @@ -1076,11 +1076,11 @@ format * pdecl_manager::pp(sort * s) const { if (i == num_params) { // all parameters are integer ptr_buffer b; - b.push_back(mk_string(m(), s->get_name().str().c_str())); + b.push_back(mk_string(m(), s->get_name().str())); for (unsigned i = 0; i < num_params; i++) b.push_back(mk_unsigned(m(), s->get_parameter(i).get_int())); return mk_seq1(m(), b.begin(), b.end(), f2f(), "_"); } } - return mk_string(m(), s->get_name().str().c_str()); + return mk_string(m(), s->get_name().str()); } diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 7fdca8cdd..927a03306 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -77,8 +77,7 @@ ATOMIC_CMD(get_user_tactics_cmd, "get-user-tactics", "display tactics defined us it->m_value->display(buf); buf << ")"; } - std::string r = buf.str(); - ctx.regular_stream() << escaped(r.c_str()); + ctx.regular_stream() << escaped(buf.str()); ctx.regular_stream() << ")\n"; }); @@ -112,7 +111,7 @@ void help_tactic(cmd_context & ctx) { probe_info * pinfo = *it2; buf << "- " << pinfo->get_name() << " " << pinfo->get_descr() << "\n"; } - ctx.regular_stream() << "\"" << escaped(buf.str().c_str()) << "\"\n"; + ctx.regular_stream() << '"' << escaped(buf.str()) << "\"\n"; } ATOMIC_CMD(help_tactic_cmd, "help-tactic", "display the tactic combinators and primitives.", help_tactic(ctx);); @@ -507,7 +506,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { throw cmd_exception("invalid using-params combinator, keyword expected", c->get_line(), c->get_pos()); if (i == num_children) throw cmd_exception("invalid using-params combinator, parameter value expected", c->get_line(), c->get_pos()); - symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str()); + symbol param_name = symbol(norm_param_name(c->get_symbol())); c = n->get_child(i); i++; switch (descrs.get_kind_in_module(param_name)) { diff --git a/src/model/model2expr.cpp b/src/model/model2expr.cpp index 4ee518282..08baffd8a 100644 --- a/src/model/model2expr.cpp +++ b/src/model/model2expr.cpp @@ -52,7 +52,7 @@ symbol mk_fresh_name::next() { _name << m_char; if (m_num > 0) _name << m_num; ++m_char; - symbol name(_name.str().c_str()); + symbol name(_name.str()); if (!m_symbols.contains(name)) { return name; } diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index ef51ec949..5a0b40657 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -107,7 +107,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod cname = mk_smt2_quoted_symbol(csym); else cname = csym.str(); - format * c_args[2] = { var, mk_string(m, cname.c_str()) }; + format * c_args[2] = { var, mk_string(m, cname) }; f_conds.push_back(mk_seq1(m, c_args, c_args+2, f2f(), "=")); } SASSERT(!f_conds.empty()); @@ -210,7 +210,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co for (unsigned j = 0; j < f->get_arity(); j++) { std::stringstream strm; strm << "x!" << (j+1); - var_names.push_back(symbol(strm.str().c_str())); + var_names.push_back(symbol(strm.str())); } } else { @@ -274,7 +274,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co def = mk_indent(m, indent, mk_compose(m, mk_compose(m, mk_string(m, "(define-fun "), - mk_string(m, fname.c_str()), + mk_string(m, fname), mk_string(m, " "), mk_compose(m, f_domain, diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h index 96c22ed29..77a186478 100644 --- a/src/model/seq_factory.h +++ b/src/model/seq_factory.h @@ -97,7 +97,7 @@ public: while (true) { std::ostringstream strm; strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim; - symbol sym(strm.str().c_str()); + symbol sym(strm.str()); if (m_strings.contains(sym)) continue; m_strings.insert(sym); return u.str.mk_string(sym); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 54cc55bd7..b70222741 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -422,7 +422,7 @@ namespace datalog { if (!e) { std::stringstream name_stm; name_stm << '#' << arg_index; - return symbol(name_stm.str().c_str()); + return symbol(name_stm.str()); } SASSERT(arg_index < e->get_data().m_value.size()); return e->get_data().m_value[arg_index]; @@ -1183,11 +1183,11 @@ namespace datalog { out << " :named "; while (fresh_names.contains(nm)) { std::ostringstream s; - s << nm << "!"; - nm = symbol(s.str().c_str()); + s << nm << '!'; + nm = symbol(s.str()); } fresh_names.add(nm); - display_symbol(out, nm) << ")"; + display_symbol(out, nm) << ')'; } out << ")\n"; } diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 87c28a34d..24604e808 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -587,7 +587,7 @@ namespace datalog { std::stringstream _name; _name << c; if (j > 0) _name << j; - symbol name(_name.str().c_str()); + symbol name(_name.str()); if (!us.contains(name)) { names.push_back(name); ++i; diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 1ab208c9e..f7f00adce 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -405,7 +405,8 @@ private: } } func_decl_ref f(m); - f = m.mk_fresh_func_decl(m_name.str().c_str(), "", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort()); + auto str = m_name.str(); + f = m.mk_fresh_func_decl(str.c_str(), "", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort()); m_fresh_predicates.push_back(f); return app_ref(m.mk_app(f, args.size(), args.c_ptr()), m); } diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 12ff2157c..a0233cc7b 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -188,7 +188,7 @@ namespace datalog { expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) { std::stringstream _name; _name << pred->get_name() << "#" << rule_id << "_" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); var_ref var = mk_index_var(); return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m); } @@ -197,7 +197,7 @@ namespace datalog { SASSERT(idx < pred->get_arity()); std::stringstream _name; _name << pred->get_name() << "#" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); expr_ref var(mk_index_var(), m); if (!is_current) { var = m_bv.mk_bv_sub(var, mk_q_one()); @@ -216,14 +216,14 @@ namespace datalog { func_decl_ref mk_q_func_decl(func_decl* f) { std::stringstream _name; _name << f->get_name() << "#"; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m); } func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id) { std::stringstream _name; _name << f->get_name() << "#" << rule_id; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m); } @@ -396,7 +396,7 @@ namespace datalog { for (unsigned i = 0; i < level_p->get_arity(); ++i) { std::stringstream _name; _name << query_pred->get_name() << "#" << level << "_" << i; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); vars.push_back(m.mk_const(nm, level_p->get_domain(i))); } return expr_ref(m.mk_app(level_p, vars.size(), vars.c_ptr()), m); @@ -569,14 +569,14 @@ namespace datalog { func_decl_ref mk_level_predicate(func_decl* p, unsigned level) { std::stringstream _name; _name << p->get_name() << "#" << level; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); } func_decl_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { std::stringstream _name; _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); } @@ -627,7 +627,7 @@ namespace datalog { func_decl_ref mk_body_func(rule& r, ptr_vector const& args, unsigned index, sort* s) { std::stringstream _name; _name << r.get_decl()->get_name() << "@" << index; - symbol name(_name.str().c_str()); + symbol name(_name.str()); func_decl* f = m.mk_func_decl(name, args.size(), args.c_ptr(), s); return func_decl_ref(f, m); } @@ -775,7 +775,7 @@ namespace datalog { func_decl_ref mk_predicate(func_decl* pred) { std::stringstream _name; _name << pred->get_name() << "#"; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); sort* pred_trace_sort = m_pred2sort.find(pred); return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); } @@ -783,7 +783,7 @@ namespace datalog { func_decl_ref mk_rule(func_decl* p, unsigned rule_idx) { std::stringstream _name; _name << "rule:" << p->get_name() << "#" << rule_idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); sort* pred_trace_sort = m_pred2sort.find(p); return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); } @@ -791,7 +791,7 @@ namespace datalog { expr_ref mk_var(func_decl* pred, sort*s, unsigned idx, expr* path_arg, expr* trace_arg) { std::stringstream _name; _name << pred->get_name() << "#V_" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); func_decl_ref fn(m); fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, s); return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); @@ -801,7 +801,7 @@ namespace datalog { SASSERT(idx < pred->get_arity()); std::stringstream _name; _name << pred->get_name() << "#X_" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); func_decl_ref fn(m); fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, pred->get_domain(idx)); return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); @@ -971,15 +971,15 @@ namespace datalog { unsigned idx = pred_idx.find(q); std::stringstream _name; _name << pred->get_name() << "_" << q->get_name() << j; - symbol name(_name.str().c_str()); + symbol name(_name.str()); type_ref tr(idx); accs.push_back(mk_accessor_decl(m, name, tr)); } std::stringstream _name; - _name << pred->get_name() << "_" << i; - symbol name(_name.str().c_str()); - _name << "?"; - symbol is_name(_name.str().c_str()); + _name << pred->get_name() << '_' << i; + symbol name(_name.str()); + _name << '?'; + symbol is_name(_name.str()); cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); } dts.push_back(mk_datatype_decl(dtu, pred->get_name(), 0, nullptr, cnstrs.size(), cnstrs.c_ptr())); @@ -1020,9 +1020,9 @@ namespace datalog { for (unsigned i = 0; i + 1 < max_arity; ++i) { std::stringstream _name; _name << "succ#" << i; - symbol name(_name.str().c_str()); + symbol name(_name.str()); _name << "?"; - symbol is_name(_name.str().c_str()); + symbol is_name(_name.str()); std::stringstream _name2; _name2 << "get_succ#" << i; ptr_vector accs; @@ -1313,7 +1313,7 @@ namespace datalog { expr_ref mk_level_predicate(symbol const& name, unsigned level) { std::stringstream _name; _name << name << "#" << level; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); } @@ -1321,21 +1321,21 @@ namespace datalog { SASSERT(idx < pred->get_arity()); std::stringstream _name; _name << pred->get_name() << "#" << level << "_" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return expr_ref(m.mk_const(nm, pred->get_domain(idx)), m); } expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) { std::stringstream _name; _name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return expr_ref(m.mk_const(nm, s), m); } expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { std::stringstream _name; _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; - symbol nm(_name.str().c_str()); + symbol nm(_name.str()); return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); } diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 3602db6d9..d5b5d42f6 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -280,7 +280,7 @@ namespace datalog { std::ostringstream strm; strm << "x" << j; bound.push_back(sig[i]); - names.push_back(symbol(strm.str().c_str())); + names.push_back(symbol(strm.str())); vars.push_back(m.mk_var(j, sig[i])); ++j; } @@ -400,8 +400,8 @@ namespace datalog { var_subst sub(m, false); for (unsigned i = 0; i < sig.size(); ++i) { std::stringstream strm; - strm << "x" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i])); + strm << 'x' << i; + vars.push_back(m.mk_const(symbol(strm.str()), sig[i])); } fml1 = sub(fml1, vars.size(), vars.c_ptr()); fml2 = sub(fml2, vars.size(), vars.c_ptr()); @@ -448,8 +448,8 @@ namespace datalog { var_subst sub(m, false); for (unsigned i = 0; i < sig.size(); ++i) { std::stringstream strm; - strm << "x" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i])); + strm << 'x' << i; + vars.push_back(m.mk_const(symbol(strm.str()), sig[i])); } fml1 = sub(fml1, vars.size(), vars.c_ptr()); fml2 = sub(fml2, vars.size(), vars.c_ptr()); diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 784a812e3..8dd7b9d26 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -373,7 +373,8 @@ namespace datalog { std::ostringstream buffer; buffer << "creating large table of size " << upper_bound; if (p) buffer << " for relation " << p->get_name(); - warning_msg("%s", buffer.str().c_str()); + auto str = buffer.str(); + warning_msg("%s", str.c_str()); } for (table_element i = 0; i < upper_bound; i++) { diff --git a/src/muz/rel/dl_lazy_table.cpp b/src/muz/rel/dl_lazy_table.cpp index 53d099532..1407aec6c 100644 --- a/src/muz/rel/dl_lazy_table.cpp +++ b/src/muz/rel/dl_lazy_table.cpp @@ -29,7 +29,7 @@ namespace datalog { symbol lazy_table_plugin::mk_name(table_plugin& p) { std::ostringstream strm; strm << "lazy_" << p.get_name(); - return symbol(strm.str().c_str()); + return symbol(strm.str()); } table_base * lazy_table_plugin::mk_empty(const table_signature & s) { diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index e809a158f..e54453d38 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -716,7 +716,7 @@ app_ref pred_transformer::mk_extend_lit() { app_ref v(m); std::stringstream name; name << m_head->get_name () << "_ext0"; - v = m.mk_const (symbol(name.str().c_str()), m.mk_bool_sort()); + v = m.mk_const (symbol(name.str()), m.mk_bool_sort()); return app_ref(m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ()))), m); } @@ -780,7 +780,7 @@ void pred_transformer::init_sig() std::stringstream name_stm; name_stm << m_head->get_name() << '_' << i; func_decl_ref stm(m); - stm = m.mk_func_decl(symbol(name_stm.str().c_str()), 0, (sort*const*)nullptr, arg_sort); + stm = m.mk_func_decl(symbol(name_stm.str()), 0, (sort*const*)nullptr, arg_sort); m_sig.push_back(pm.get_o_pred(stm, 0)); } } @@ -1025,7 +1025,7 @@ app_ref pred_transformer::mk_fresh_rf_tag () func_decl_ref decl(m); name << head ()->get_name () << "#reach_tag_" << m_reach_facts.size (); - decl = m.mk_func_decl (symbol (name.str ().c_str ()), 0, + decl = m.mk_func_decl (symbol(name.str()), 0, (sort*const*)nullptr, m.mk_bool_sort ()); return app_ref(m.mk_const (pm.get_n_pred (decl)), m); } @@ -1628,7 +1628,7 @@ void pred_transformer::init_rules(decl2rel const& pts) { for (auto &kv : m_pt_rules) { pt_rule &r = *kv.m_value; std::string name = head()->get_name().str() + "__tr" + std::to_string(i); - tag = m.mk_const(symbol(name.c_str()), m.mk_bool_sort()); + tag = m.mk_const(symbol(name), m.mk_bool_sort()); m_pt_rules.set_tag(tag, r); m_transition_clause.push_back(tag); transitions.push_back(m.mk_implies(r.tag(), r.trans())); @@ -1823,7 +1823,8 @@ app* pred_transformer::extend_initial (expr *e) app_ref v(m); std::stringstream name; name << m_head->get_name() << "_ext"; - v = m.mk_fresh_const (name.str ().c_str (), + auto str = name.str (); + v = m.mk_fresh_const (str.c_str(), m.mk_bool_sort ()); v = m.mk_const (pm.get_n_pred (v->get_decl ())); diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index f560ef4dd..ba20e5f24 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -180,7 +180,7 @@ func_decl * manager::get_n_pred(func_decl* s) { app* mk_zk_const(ast_manager &m, unsigned idx, sort *s) { std::stringstream name; name << "sk!" << idx; - return m.mk_const(symbol(name.str().c_str()), s); + return m.mk_const(symbol(name.str()), s); } namespace find_zk_const_ns { diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 4899ad692..e2daa3ac4 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -79,7 +79,8 @@ void prop_solver::add_level() unsigned idx = level_cnt(); std::stringstream name; name << m_name << "#level_" << idx; - func_decl * lev_pred = m.mk_fresh_func_decl(name.str().c_str(), 0, nullptr, m.mk_bool_sort()); + auto str = name.str(); + func_decl * lev_pred = m.mk_fresh_func_decl(str.c_str(), 0, nullptr, m.mk_bool_sort()); m_level_preds.push_back(lev_pred); app_ref pos_la(m.mk_const(lev_pred), m); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 504acf753..3843123a1 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -116,7 +116,7 @@ namespace datalog { SASSERT(tail.size()==tail_neg.size()); std::ostringstream comb_name; comb_name << tgt.name().str() << ";" << src.name().str(); - symbol combined_rule_name = symbol(comb_name.str().c_str()); + symbol combined_rule_name(comb_name.str()); res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), combined_rule_name, m_normalize); res->set_accounting_parent_object(m_context, const_cast(&tgt)); TRACE("dl", diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index c9d4fd3c6..67ae26a8d 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -71,7 +71,7 @@ namespace datalog { std::stringstream name_suffix; name_suffix << "compr_arg_" << arg_index; - func_decl * cpred = m_context.mk_fresh_head_predicate(parent_name, symbol(name_suffix.str().c_str()), + func_decl * cpred = m_context.mk_fresh_head_predicate(parent_name, symbol(name_suffix.str()), arity, domain.c_ptr(), pred); m_pinned.push_back(cpred); m_pinned.push_back(pred); diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 599f248e8..0efda9baa 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -365,7 +365,7 @@ public: //expr* x = m_x2t->find(ra->x()); std::ostringstream strm; s.display(strm, l.sign()?~l:l); - result = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); + result = m.mk_const(symbol(strm.str()), m.mk_bool_sort()); } } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index f116da8e5..f93039c21 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -251,7 +251,8 @@ namespace opt { m_msolver = mk_sortmax(m_c, m_weights, m_soft_constraints); } else { - warning_msg("solver %s is not recognized, using default 'maxres'", maxsat_engine.str().c_str()); + auto str = maxsat_engine.str(); + warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str()); m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e69ac51d3..940dba8d5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -665,9 +665,8 @@ namespace opt { opt_params p(m_params); if (p.optsmt_engine() == symbol("symba") || p.optsmt_engine() == symbol("farkas")) { - std::stringstream strm; - strm << AS_OPTINF; - gparams::set("smt.arith.solver", strm.str().c_str()); + auto str = std::to_string(AS_OPTINF); + gparams::set("smt.arith.solver", str.c_str()); } } @@ -693,7 +692,7 @@ namespace opt { expr_ref_vector fmls(m); get_solver().get_assertions(fmls); m_sat_solver->assert_expr(fmls); - m_solver = m_sat_solver.get(); + m_solver = m_sat_solver.get(); } void context::enable_sls(bool force) { @@ -950,8 +949,8 @@ namespace opt { tout << "offset: " << offset << "\n"; ); std::ostringstream out; - out << orig_term << ":" << index; - id = symbol(out.str().c_str()); + out << orig_term << ':' << index; + id = symbol(out.str()); return true; } if (is_max && get_pb_sum(term, terms, weights, offset)) { @@ -973,8 +972,8 @@ namespace opt { } neg = true; std::ostringstream out; - out << orig_term << ":" << index; - id = symbol(out.str().c_str()); + out << orig_term << ':' << index; + id = symbol(out.str()); return true; } if ((is_max || is_min) && m_bv.is_bv(term)) { @@ -992,9 +991,9 @@ namespace opt { } neg = is_max; std::ostringstream out; - out << orig_term << ":" << index; - id = symbol(out.str().c_str()); - return true; + out << orig_term << ':' << index; + id = symbol(out.str()); + return true; } return false; } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 97aa54d4a..d7a27fbb7 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -175,7 +175,7 @@ namespace opt { w.start(); std::stringstream file_name; file_name << "opt_solver" << ++m_dump_count << ".smt2"; - std::ofstream buffer(file_name.str().c_str()); + std::ofstream buffer(file_name.str()); to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver"); buffer.close(); IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "..."; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 0b722832a..c41d8490b 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -836,7 +836,7 @@ namespace smt2 { symbol ct_name = curr_id(); std::string r_str = "is-"; r_str += curr_id().str(); - symbol r_name(r_str.c_str()); + symbol r_name(r_str); next(); TRACE("datatype_parser_bug", tout << ct_name << " " << r_name << "\n";); ct_decls.push_back(pm().mk_pconstructor_decl(m_sort_id2param_idx.size(), ct_name, r_name, 0, nullptr)); @@ -847,7 +847,7 @@ namespace smt2 { symbol ct_name = curr_id(); std::string r_str = "is-"; r_str += curr_id().str(); - symbol r_name(r_str.c_str()); + symbol r_name(r_str); next(); paccessor_decl_ref_buffer new_a_decls(pm()); parse_accessor_decls(new_a_decls); @@ -1148,7 +1148,8 @@ namespace smt2 { else { std::ostringstream str; str << "unknown attribute " << id; - warning_msg("%s", str.str().c_str()); + auto msg = str.str(); + warning_msg("%s", msg.c_str()); next(); // just consume the consume_sexpr(); diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index df1f6cd00..d9b3937ea 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -58,7 +58,8 @@ struct pattern_validation_functor { void operator()(app * n) { func_decl * decl = to_app(n)->get_decl(); if (is_forbidden(decl)) { - warning_msg("(%d,%d): '%s' cannot be used in patterns.", m_line, m_pos, decl->get_name().str().c_str()); + auto str = decl->get_name().str(); + warning_msg("(%d,%d): '%s' cannot be used in patterns.", m_line, m_pos, str.c_str()); m_result = false; } } diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 5d7bdaf14..949b4c504 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -1083,7 +1083,7 @@ namespace qe { for (expr * x : m_idxs[0].idx) { std::stringstream name; name << "get" << (i++); - acc.push_back(mk_accessor_decl(m, symbol(name.str().c_str()), type_ref(m.get_sort(x)))); + acc.push_back(mk_accessor_decl(m, symbol(name.str()), type_ref(m.get_sort(x)))); } constructor_decl* constrs[1] = { mk_constructor_decl(symbol("tuple"), symbol("is-tuple"), acc.size(), acc.c_ptr()) }; datatype::def* dts = mk_datatype_decl(dt, symbol("tuple"), 0, nullptr, 1, constrs); diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index 85bb14640..fb1afc4c2 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -76,7 +76,8 @@ namespace qe { func_decl* f = m_val->get_decl(); ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned i = 0; i < acc.size(); ++i) { - arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range()); + auto str = acc[i]->get_name().str(); + arg = m.mk_fresh_const(str.c_str(), acc[i]->get_range()); vars.push_back(arg); model.register_decl(arg->get_decl(), m_val->get_arg(i)); args.push_back(arg); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 54eb008ca..d87befcf9 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -38,7 +38,7 @@ namespace sat { { if (s.get_config().m_drat && s.get_config().m_drat_file != symbol()) { auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out; - m_out = alloc(std::ofstream, s.get_config().m_drat_file.str().c_str(), mode); + m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode); if (s.get_config().m_drat_binary) { std::swap(m_out, m_bout); } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 9730334b9..20484ae28 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -206,8 +206,7 @@ public: catch (z3_exception& ex) { IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";); reason_set = true; - std::string msg = std::string("(sat.giveup ") + ex.msg() + std::string(")"); - set_reason_unknown(msg.c_str()); + set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')'); r = l_undef; } switch (r) { @@ -500,6 +499,10 @@ public: m_unknown = msg; } + void set_reason_unknown(std::string &&msg) { + m_unknown = std::move(msg); + } + void get_labels(svector & r) override { } @@ -656,7 +659,7 @@ private: strm << "(sat.giveup interpreted atoms sent to SAT solver " << atoms <<")"; TRACE("sat", tout << strm.str() << "\n";); IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";); - set_reason_unknown(strm.str().c_str()); + set_reason_unknown(strm.str()); return l_undef; } return l_true; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 1ae97bba1..a5426b2a6 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1125,7 +1125,7 @@ namespace smt { ast_manager& m = get_manager(); std::ostringstream strm; strm << val << " <= " << mk_pp(get_enode(v)->get_owner(), get_manager()); - app* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); + app* b = m.mk_const(symbol(strm.str()), m.mk_bool_sort()); expr_ref result(b, m); TRACE("opt", tout << result << "\n";); if (!ctx.b_internalized(b)) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 071496577..0722244ff 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1995,7 +1995,7 @@ public: expr_ref var2expr(lpvar v) { std::ostringstream name; name << "v" << lp().local_to_external(v); - return expr_ref(m.mk_const(symbol(name.str().c_str()), a.mk_int()), m); + return expr_ref(m.mk_const(symbol(name.str()), a.mk_int()), m); } expr_ref multerm(rational const& r, expr* e) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 0ba9e7851..1202f77c0 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1949,7 +1949,7 @@ public: else { strm << val; } - zstring zs(strm.str().c_str()); + zstring zs(strm.str()); add_buffer(sbuffer, zs); break; } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4e560cec6..32667f438 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -988,7 +988,7 @@ namespace smt { } } if (constOK) { - TRACE("str", tout << "flattened to \"" << flattenedString.encode().c_str() << "\"" << std::endl;); + TRACE("str", tout << "flattened to \"" << flattenedString.encode() << '"' << std::endl;); expr_ref constStr(mk_string(flattenedString), m); expr_ref axiom(ctx.mk_eq_atom(a_cat, constStr), m); assert_axiom(axiom); @@ -1073,7 +1073,7 @@ namespace smt { zstring strconst; u.str.is_string(str->get_owner(), strconst); - TRACE("str", tout << "instantiating constant string axioms for \"" << strconst.encode().c_str() << "\"" << std::endl;); + TRACE("str", tout << "instantiating constant string axioms for \"" << strconst.encode() << '"' << std::endl;); unsigned int l = strconst.length(); expr_ref len(m_autil.mk_numeral(rational(l), true), m); @@ -8177,7 +8177,7 @@ namespace smt { if (!Ival.is_minus_one()) { rational Slen; if (get_len_value(S, Slen)) { - zstring Ival_str(Ival.to_string().c_str()); + zstring Ival_str(Ival.to_string()); if (rational(Ival_str.length()) <= Slen) { zstring padding; for (rational i = rational::zero(); i < Slen - rational(Ival_str.length()); ++i) { @@ -8301,7 +8301,7 @@ namespace smt { conclusion = expr_ref(ctx.mk_eq_atom(a, mk_string("")), m); } else { // non-negative argument -> convert to string of digits - zstring Nval_str(Nval.to_string().c_str()); + zstring Nval_str(Nval.to_string()); conclusion = expr_ref(ctx.mk_eq_atom(a, mk_string(Nval_str)), m); } expr_ref axiom(rewrite_implication(premise, conclusion), m); @@ -8885,19 +8885,6 @@ namespace smt { return FC_CONTINUE; // since by this point we've added axioms } - inline zstring int_to_string(int i) { - std::stringstream ss; - ss << i; - std::string str = ss.str(); - return zstring(str.c_str()); - } - - inline std::string longlong_to_string(long long i) { - std::stringstream ss; - ss << i; - return ss.str(); - } - void theory_str::get_concats_in_eqc(expr * n, std::set & concats) { expr * eqcNode = n; @@ -9016,7 +9003,7 @@ namespace smt { TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); std::ostringstream unused; unused << "**UNUSED**" << (m_unused_id++); - return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str()))); + return alloc(expr_wrapper_proc, to_app(mk_string(unused.str()))); } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 214ad0efa..b80a5e3e7 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -65,7 +65,7 @@ public: while (true) { std::ostringstream strm; strm << delim << std::hex << (m_next++) << std::dec << delim; - symbol sym(strm.str().c_str()); + symbol sym(strm.str()); if (m_strings.contains(sym)) continue; m_strings.insert(sym); return u.str.mk_string(sym); @@ -343,7 +343,8 @@ class theory_str : public theory { typedef map, default_eq > rational_map; struct zstring_hash_proc { unsigned operator()(zstring const & s) const { - return string_hash(s.encode().c_str(), static_cast(s.length()), 17); + auto str = s.encode(); + return string_hash(str.c_str(), static_cast(s.length()), 17); } }; typedef map > string_map; diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 3563f5a72..ff66b2172 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -32,19 +32,6 @@ namespace smt { - inline zstring int_to_string(int i) { - std::stringstream ss; - ss << i; - std::string str = ss.str(); - return zstring(str.c_str()); - } - - inline std::string longlong_to_string(long long i) { - std::stringstream ss; - ss << i; - return ss.str(); - } - /* * Use the current model in the arithmetic solver to get the length of a term. * Returns true if this could be done, placing result in 'termLen', or false otherwise. @@ -780,7 +767,7 @@ namespace smt { return false; } // convert iValue to a constant - zstring iValue_str = zstring(iValue.to_string().c_str()); + zstring iValue_str(iValue.to_string()); for (unsigned idx = 0; idx < iValue_str.length(); ++idx) { expr_ref chTerm(bitvector_character_constants.get(iValue_str[idx]), sub_m); eqc_chars.push_back(chTerm); @@ -1135,7 +1122,7 @@ namespace smt { TRACE("str_fl", tout << "integer theory assigns " << ival << " to " << mk_pp(e, get_manager()) << std::endl;); // if ival is non-negative, because we know the length of arg, we can add a character constraint for arg if (ival.is_nonneg()) { - zstring ival_str(ival.to_string().c_str()); + zstring ival_str(ival.to_string()); zstring padding; for (rational i = rational::zero(); i < slen - rational(ival_str.length()); ++i) { padding = padding + zstring("0"); @@ -1176,7 +1163,7 @@ namespace smt { ival_str = zstring(""); } else { // e must be equal to the string representation of ival - ival_str = zstring(ival.to_string().c_str()); + ival_str = zstring(ival.to_string()); } // Add (arg == ival) as a precondition. precondition.push_back(m.mk_eq(arg, mk_int(ival))); diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 8ff1370a2..27fe14da5 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -234,9 +234,10 @@ namespace smt { return; } std::stringstream msg; - msg << "found non utvpi logic expression:\n" << mk_pp(n, m) << "\n"; - TRACE("utvpi", tout << msg.str();); - warning_msg("%s", msg.str().c_str()); + msg << "found non utvpi logic expression:\n" << mk_pp(n, m) << '\n'; + auto str = msg.str(); + TRACE("utvpi", tout << str;); + warning_msg("%s", str.c_str()); ctx.push_trail(value_trail(m_non_utvpi_exprs)); m_non_utvpi_exprs = true; } diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index d1021da3e..16764ba56 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -395,7 +395,7 @@ solver* solver_pool::mk_solver() { } std::stringstream name; name << "vsolver#" << m_solvers.size(); - app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m); + app_ref pred(m.mk_const(symbol(name.str()), m.mk_bool_sort()), m); pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred); m_solvers.push_back(solver); return solver; diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp index ecf0cbe4d..8bd41372c 100644 --- a/src/test/expr_rand.cpp +++ b/src/test/expr_rand.cpp @@ -42,7 +42,7 @@ void tst_expr_arith(unsigned num_files) { std::ostringstream buffer; buffer << "random_arith_" << i << ".smt2"; std::cout << buffer.str() << "\n"; - std::ofstream file(buffer.str().c_str()); + std::ofstream file(buffer.str()); pp.display_smt2(file, e.get()); file.close(); } @@ -85,7 +85,7 @@ void tst_expr_rand(unsigned num_files) { std::ostringstream buffer; buffer << "random_bv_" << i << ".smt2"; std::cout << buffer.str() << "\n"; - std::ofstream file(buffer.str().c_str()); + std::ofstream file(buffer.str()); pp.display_smt2(file, e.get()); file.close(); diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index bf059ee10..752a9a089 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -140,7 +140,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) { name << "u" << i; increments.push_back(tmp); vars.push_back(var); - names.push_back(symbol(name.str().c_str())); + names.push_back(symbol(name.str())); sorts.push_back(a.mk_int()); } } diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index 623f7c9f1..2d83ad87d 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -31,7 +31,7 @@ static void test1() { for (unsigned i = 0; i < N; ++i) { std::stringstream strm; strm << "b" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort())); } for (unsigned k = 1; k <= N; ++k) { @@ -112,7 +112,7 @@ static void test2() { for (unsigned i = 0; i < N; ++i) { std::stringstream strm; strm << "b" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort())); } for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { vector coeffs; @@ -181,7 +181,7 @@ static void test3() { for (unsigned i = 0; i < N; ++i) { std::stringstream strm; strm << "b" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort())); } for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { vector coeffs; diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 2b1b9686c..a6891a298 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -288,7 +288,7 @@ static void mk_var(unsigned x, app_ref& v) { arith_util a(m); std::ostringstream strm; strm << "v" << x; - v = m.mk_const(symbol(strm.str().c_str()), a.mk_real()); + v = m.mk_const(symbol(strm.str()), a.mk_real()); } static void mk_term(vector const& vars, rational const& coeff, app_ref& term) { diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp index 3188b1a6a..1c23c1eaa 100644 --- a/src/test/theory_pb.cpp +++ b/src/test/theory_pb.cpp @@ -40,7 +40,7 @@ public: for (unsigned i = 0; i < N; ++i) { std::stringstream strm; strm << "b" << i; - vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort())); std::cout << "(declare-const " << strm.str() << " Bool)\n"; } } diff --git a/src/util/string_buffer.h b/src/util/string_buffer.h index 14f4d1cdf..7faaedc78 100644 --- a/src/util/string_buffer.h +++ b/src/util/string_buffer.h @@ -78,6 +78,16 @@ public: m_pos += len; } + void append(const std::string &str) { + size_t len = str.size(); + size_t new_pos = m_pos + len; + while (new_pos > m_capacity) { + expand(); + } + memcpy(m_buffer + m_pos, str.c_str(), len); + m_pos += len; + } + void append(int n) { auto str = std::to_string(n); append(str.c_str()); @@ -121,6 +131,12 @@ inline string_buffer & operator<<(string_buffer & buffer, const char * s return buffer; } +template +inline string_buffer & operator<<(string_buffer & buffer, const std::string &str) { + buffer.append(str); + return buffer; +} + template inline string_buffer & operator<<(string_buffer & buffer, char c) { buffer.append(c); diff --git a/src/util/symbol.h b/src/util/symbol.h index 5dba08669..9fe40d83a 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -20,8 +20,9 @@ Revision History: // include "util/new_symbol.h" #else #pragma once -#include -#include +#include +#include +#include #include "util/util.h" #include "util/tptr.h" @@ -56,6 +57,7 @@ public: m_data(nullptr) { } explicit symbol(char const * d); + explicit symbol(const std::string & str) : symbol(str.c_str()) {} explicit symbol(unsigned idx): m_data(BOXTAGINT(char const *, idx, 1)) { #if !defined(__LP64__) && !defined(_WIN64) diff --git a/src/util/util.h b/src/util/util.h index 5860382c6..c0dd51d81 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -24,6 +24,7 @@ Revision History: #include #include #include +#include #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -375,6 +376,7 @@ class escaped { char const * end() const; public: escaped(char const * str, bool trim_nl = false, unsigned indent = 0):m_str(str), m_trim_nl(trim_nl), m_indent(indent) {} + escaped(const std::string &str, bool trim_nl = false, unsigned indent = 0):m_str(str.c_str()), m_trim_nl(trim_nl), m_indent(indent) {} void display(std::ostream & out) const; };