mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

remove some allocs from exceptions

Browse source
This commit is contained in:
Nuno Lopes 2018-07-02 17:08:02 +01:00
parent 8791f61aa7
commit cef17c22a1
19 changed files with 36 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -968,7 +968,7 @@ private:
void throw_tactic(expr* e) {
std::stringstream strm;
strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
throw tactic_exception(strm.str().c_str());
throw tactic_exception(strm.str());
}
};

6
src/tactic/tactic.cpp
View file

@ -206,7 +206,7 @@ void fail_if_proof_generation(char const * tactic_name, goal_ref const & in) {
if (in->proofs_enabled()) {
std::string msg = tactic_name;
msg += " does not support proof production";
throw tactic_exception(msg.c_str());
throw tactic_exception(std::move(msg));
}
}
@ -214,7 +214,7 @@ void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in
if (in->unsat_core_enabled()) {
std::string msg = tactic_name;
msg += " does not support unsat core production";
throw tactic_exception(msg.c_str());
throw tactic_exception(std::move(msg));
}
}
@ -222,6 +222,6 @@ void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
if (in->models_enabled()) {
std::string msg = tactic_name;
msg += " does not generate models";
throw tactic_exception(msg.c_str());
throw tactic_exception(std::move(msg));
}
}

2
src/tactic/tactic_exception.h
View file

@ -26,7 +26,7 @@ class tactic_exception : public z3_exception {
protected:
std::string m_msg;
public:
tactic_exception(char const * msg):m_msg(msg) {}
tactic_exception(std::string && msg) : m_msg(std::move(msg)) {}
~tactic_exception() override {}
char const * msg() const override { return m_msg.c_str(); }
};

8
src/tactic/tactical.cpp
View file

@ -463,9 +463,9 @@ public:
if (finished_id == UINT_MAX) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
case TACTIC_EX: throw tactic_exception(ex_msg.c_str());
case TACTIC_EX: throw tactic_exception(std::move(ex_msg));
default:
throw default_exception(ex_msg.c_str());
throw default_exception(std::move(ex_msg));
}
}
}
@ -660,9 +660,9 @@ public:
if (failed) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
case TACTIC_EX: throw tactic_exception(ex_msg.c_str());
case TACTIC_EX: throw tactic_exception(std::move(ex_msg));
default:
throw default_exception(ex_msg.c_str());
throw default_exception(std::move(ex_msg));
}
}