diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 44c423c09..211c67953 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -141,7 +141,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects to take as many arguments as the function being mapped, " << "it was given " << arity << " but expects " << f->get_arity(); - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } if (arity == 0) { @@ -158,14 +158,14 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* if (!is_array_sort(domain[i])) { std::ostringstream buffer; buffer << "map expects an array sort as argument at position " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } if (get_array_arity(domain[i]) != dom_arity) { std::ostringstream buffer; buffer << "map expects all arguments to have the same array domain, " << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } for (unsigned j = 0; j < dom_arity; ++j) { @@ -173,7 +173,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects all arguments to have the same array domain, " << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } } @@ -181,7 +181,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects the argument at position " << i << " to have the array range the same as the function"; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } } @@ -244,7 +244,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { if (num_parameters != arity) { std::stringstream strm; strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments"; - m_manager->raise_exception(strm.str().c_str()); + m_manager->raise_exception(strm.str()); return nullptr; } ptr_buffer new_domain; // we need this because of coercions. @@ -256,7 +256,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { std::stringstream strm; strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter "; strm << parameter_pp(parameters[i], *m_manager) << " do not match"; - m_manager->raise_exception(strm.str().c_str()); + m_manager->raise_exception(strm.str()); UNREACHABLE(); return nullptr; } @@ -284,7 +284,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { std::ostringstream buffer; buffer << "store expects the first argument to be an array taking " << num_parameters+1 << ", instead it was passed " << (arity - 1) << "arguments"; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); UNREACHABLE(); return nullptr; } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b84dac136..c73e2f1d8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1584,8 +1584,8 @@ void ast_manager::raise_exception(char const * msg) { throw ast_exception(msg); } -void ast_manager::raise_exception(std::string const& msg) { - throw ast_exception(msg.c_str()); +void ast_manager::raise_exception(std::string && msg) { + throw ast_exception(std::move(msg)); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 9c6c811b0..1c25ff9ec 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1574,7 +1574,7 @@ public: // Equivalent to throw ast_exception(msg) Z3_NORETURN void raise_exception(char const * msg); - Z3_NORETURN void raise_exception(std::string const& s); + Z3_NORETURN void raise_exception(std::string && s); std::ostream& display(std::ostream& out, parameter const& p); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index ea220f7e7..48daf6988 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -951,7 +951,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { strm << "(set-logic " << m_logic << ")\n"; } if (!m_attributes.empty()) { - strm << "; " << m_attributes.c_str(); + strm << "; " << m_attributes; } #if 0 diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 738444b3b..4ffd7d6cb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -624,7 +624,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p if (m.get_sort(args[i]) != r->get_domain(i)) { std::ostringstream buffer; buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); - m.raise_exception(buffer.str().c_str()); + m.raise_exception(buffer.str()); return nullptr; } } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8bf0abbb3..146c7359f 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -342,7 +342,7 @@ namespace datatype { std::ostringstream buffer; buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) << " instead of " << mk_ismt2_pp(domain[1], m); - m.raise_exception(buffer.str().c_str()); + m.raise_exception(buffer.str()); return nullptr; } range = domain[0]; diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 01b06518e..43cf50662 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -54,7 +54,7 @@ namespace datalog { } std::ostringstream buffer; buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return false; } @@ -676,7 +676,7 @@ namespace datalog { } std::stringstream strm; strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); return nullptr; } diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index 65250282c..f6f2d6f85 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -86,7 +86,7 @@ struct enum2bv_rewriter::imp { void throw_non_fd(expr* e) { std::stringstream strm; strm << "unable to handle nested data-type expression " << mk_pp(e, m); - throw rewriter_exception(strm.str().c_str()); + throw rewriter_exception(strm.str()); } void check_for_fd(unsigned n, expr* const* args) { diff --git a/src/ast/rewriter/rewriter_types.h b/src/ast/rewriter/rewriter_types.h index 094357fed..77ab42b2a 100644 --- a/src/ast/rewriter/rewriter_types.h +++ b/src/ast/rewriter/rewriter_types.h @@ -46,7 +46,7 @@ inline br_status unsigned2br_status(unsigned u) { class rewriter_exception : public default_exception { public: - rewriter_exception(char const * msg):default_exception(msg) {} + rewriter_exception(std::string && msg) : default_exception(std::move(msg)) {} }; #endif diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 20e1fb36c..7576e43c0 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -400,7 +400,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do std::ostringstream strm; strm << "Unexpected number of arguments to '" << sig.m_name << "' "; strm << "at least one argument expected " << dsz << " given"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -420,7 +420,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do if (range) { strm << " and range: " << mk_pp(range, m); } - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } range_out = apply_binding(binding, sig.m_range); SASSERT(range_out); @@ -434,7 +434,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran std::ostringstream strm; strm << "Unexpected number of arguments to '" << sig.m_name << "' "; strm << sig.m_dom.size() << " arguments expected " << dsz << " given"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -459,13 +459,13 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran strm << mk_pp(sig.m_dom[i].get(), m) << " "; } - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } if (!range && dsz == 0) { std::ostringstream strm; strm << "Sort of polymorphic function '" << sig.m_name << "' "; strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } range_out = apply_binding(m_binding, sig.m_range); SASSERT(range_out); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c58453460..9de183ca8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -797,7 +797,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { msg += " '"; msg += s.str(); msg += "' (with the given signature) already declared"; - throw cmd_exception(msg.c_str()); + throw cmd_exception(std::move(msg)); } if (s != f->get_name()) { TRACE("func_decl_alias", tout << "adding alias for: " << f->get_name() << ", alias: " << s << "\n";); @@ -1142,7 +1142,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg for (unsigned i = 0; i < fs.get_num_entries(); ++i) { buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " "; } - throw cmd_exception(buffer.str().c_str()); + throw cmd_exception(buffer.str()); } if (well_sorted_check_enabled()) m().check_sort(f, num_args, args); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index bf1e25e57..c103b0276 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -482,7 +482,7 @@ namespace smt2 { if (context[0]) msg += ": "; msg += "unknown sort '"; msg += id.str() + "'"; - throw parser_exception(msg.c_str()); + throw parser_exception(std::move(msg)); } void consume_sexpr() { @@ -1633,7 +1633,7 @@ namespace smt2 { void unknown_var_const_name(symbol id) { std::string msg = "unknown constant/variable '"; msg += id.str() + "'"; - throw parser_exception(msg.c_str()); + throw parser_exception(std::move(msg)); } rational m_last_bv_numeral; // for bv, bvbin, bvhex @@ -2431,7 +2431,7 @@ namespace smt2 { buffer << "invalid function definition, sort mismatch. Expcected " << mk_pp(f->get_range(), m()) << " but function body has sort " << mk_pp(m().get_sort(body), m()); - throw parser_exception(buffer.str().c_str()); + throw parser_exception(buffer.str()); } m_ctx.insert_rec_fun(f, bindings, ids, body); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 008da06ec..d0ca05ff9 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -173,7 +173,7 @@ namespace smt { if (num_instances > 0) { out << "[quantifier_instances] "; out.width(10); - out << q->get_qid().str().c_str() << " : "; + out << q->get_qid().str() << " : "; out.width(6); out << num_instances << " : "; out.width(3); diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 9ab3123a2..6b5919f8e 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -172,7 +172,7 @@ public: } for (unsigned i = 0; i < n; i++) { if (tmp[i] == '.') { - param_name = tmp.substr(i+1).c_str(); + param_name = tmp.c_str() + i + 1; tmp.resize(i); mod_name = tmp.c_str(); return;