mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
move a few strings instead of copying
This commit is contained in:
parent
2417bedb98
commit
6a0c409b0f
|
@ -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<sort> 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;
|
||||
}
|
||||
|
|
|
@ -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));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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];
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
@ -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) {
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue