3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

Catch exceptions by const-reference

Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
This commit is contained in:
Michał Janiszewski 2018-10-12 21:15:31 +02:00
parent b301a59899
commit cfd0486582
36 changed files with 45 additions and 45 deletions

View file

@ -231,7 +231,7 @@ namespace datatype {
}
return s;
}
catch (invalid_datatype) {
catch (const invalid_datatype &) {
m_manager->raise_exception("invalid datatype");
return nullptr;
}

View file

@ -58,7 +58,7 @@ bool has_skolem_functions(expr * n) {
try {
for_each_expr(p, n);
}
catch (has_skolem_functions_ns::found) {
catch (const has_skolem_functions_ns::found &) {
return true;
}
return false;

View file

@ -58,7 +58,7 @@ bool occurs(expr * n1, expr * n2) {
try {
quick_for_each_expr(p, n2);
}
catch (occurs_namespace::found) {
catch (const occurs_namespace::found &) {
return true;
}
return false;
@ -69,7 +69,7 @@ bool occurs(func_decl * d, expr * n) {
try {
quick_for_each_expr(p, n);
}
catch (occurs_namespace::found) {
catch (const occurs_namespace::found &) {
return true;
}
return false;

View file

@ -476,7 +476,7 @@ struct check_logic::imp {
quick_for_each_expr(*this, n);
return true;
}
catch (failed) {
catch (const failed &) {
return false;
}
}
@ -495,7 +495,7 @@ struct check_logic::imp {
check_sort(f->get_range());
return true;
}
catch (failed) {
catch (const failed &) {
return false;
}
}

View file

@ -1833,7 +1833,7 @@ void cmd_context::validate_model() {
for_each_expr(contains_underspecified, a);
for_each_expr(contains_underspecified, r);
}
catch (contains_underspecified_op_proc::found) {
catch (const contains_underspecified_op_proc::found &) {
continue;
}
TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0););

View file

@ -1989,7 +1989,7 @@ namespace algebraic_numbers {
TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";);
return qm().sign(r);
}
catch (opt_var2basic::failed) {
catch (const opt_var2basic::failed &) {
// continue
}

View file

@ -4493,7 +4493,7 @@ namespace polynomial {
}
#endif
}
catch (sparse_mgcd_failed) {
catch (const sparse_mgcd_failed &) {
flet<bool> use_prs(m_use_prs_gcd, false);
gcd_prs(u, v, x, r);
}

View file

@ -183,7 +183,7 @@ class subpaving_tactic : public tactic {
process_clause(g.form(i));
}
}
catch (subpaving::exception) {
catch (const subpaving::exception &) {
throw tactic_exception("failed to internalize goal into subpaving module");
}
}
@ -195,7 +195,7 @@ class subpaving_tactic : public tactic {
try {
(*m_ctx)();
}
catch (subpaving::exception) {
catch (const subpaving::exception &) {
throw tactic_exception("failed building subpaving tree...");
}
if (m_display) {

View file

@ -422,7 +422,7 @@ namespace datalog {
try {
quick_for_each_expr(proc, fml);
}
catch (contains_predicate_proc::found) {
catch (const contains_predicate_proc::found &) {
return true;
}
return false;

View file

@ -219,7 +219,7 @@ private:
quick_for_each_expr(m_proc, m_mark1, fml);
m_mark1.reset();
}
catch (contains_predicate_proc::found) {
catch (const contains_predicate_proc::found &) {
m_mark1.reset();
return true;
}

View file

@ -2737,7 +2737,7 @@ lbool context::solve(unsigned from_lvl)
// }
}
VERIFY (validate ());
} catch (unknown_exception)
} catch (const unknown_exception &)
{}
if (m_last_result == l_true) {

View file

@ -95,7 +95,7 @@ bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e, ast_manag
is_pure_expr_proc proc(symbs, m);
try {
for_each_expr(proc, e);
} catch (is_pure_expr_proc::non_pure) {
} catch (const is_pure_expr_proc::non_pure &) {
return false;
}
return true;

View file

@ -88,7 +88,7 @@ bool iuc_proof::is_core_pure(expr* e) const
try {
for_each_expr(proc, e);
}
catch (is_pure_expr_proc::non_pure)
catch (const is_pure_expr_proc::non_pure &)
{return false;}
return true;

View file

@ -247,7 +247,7 @@ bool has_zk_const(expr *e){
try {
for_each_expr(p, e);
}
catch (has_zk_const_ns::found) {
catch (const has_zk_const_ns::found &) {
return true;
}
return false;

View file

@ -120,7 +120,7 @@ struct index_lt_proc : public std::binary_function<app*, app *, bool> {
for (expr *e : v)
quick_for_each_expr(fn, visited, e);
}
catch (has_nlira_functor::found ) {
catch (const has_nlira_functor::found &) {
return true;
}
return false;

View file

@ -891,7 +891,7 @@ namespace {
for_each_expr(cs, fml);
return false;
}
catch(found) {
catch(const found &) {
return true;
}
}

View file

@ -415,7 +415,7 @@ namespace tb {
try {
quick_for_each_expr(p, t);
}
catch (non_constructor) {
catch (const non_constructor &) {
return false;
}
return true;

View file

@ -57,7 +57,7 @@ namespace {
term_ite_proc f(m);
try {
quick_for_each_expr(f, e);
} catch (term_ite_proc::found) {
} catch (const term_ite_proc::found &) {
return true;
}
return false;

View file

@ -706,7 +706,7 @@ namespace opt {
quick_for_each_expr(proc, visited, f);
}
}
catch (is_bv::found) {
catch (const is_bv::found &) {
return false;
}
return true;
@ -737,7 +737,7 @@ namespace opt {
try {
quick_for_each_expr(proc, visited, p);
}
catch (is_propositional_fn::found) {
catch (const is_propositional_fn::found &) {
return false;
}
return true;

View file

@ -3084,7 +3084,7 @@ namespace smt2 {
<< ": " << ex.msg() << "\")" << std::endl;
exit(ex.error_code());
}
catch (stop_parser_exception) {
catch (const stop_parser_exception &) {
m_scanner.stop_caching();
return !found_errors;
}

View file

@ -118,7 +118,7 @@ bool simple_parser::parse(std::istream & in, expr_ref & result) {
if (!result)
throw parser_error();
}
catch (parser_error) {
catch (const parser_error &) {
warning_msg("parser error");
return false;
}

View file

@ -61,7 +61,7 @@ namespace qe {
project_nonrec(model, vars, lits);
}
}
catch (cant_project) {
catch (const cant_project &) {
TRACE("qe", tout << "can't project:" << mk_pp(var, m) << "\n";);
return false;
}

View file

@ -62,7 +62,7 @@ namespace qe {
is_pure_ns::proc v(is_var);
quick_for_each_expr(v, e);
}
catch (is_pure_ns::found) {
catch (const is_pure_ns::found &) {
return false;
}
return true;

View file

@ -87,7 +87,7 @@ namespace sat {
try {
return apply_rec(arg1, arg2, op);
}
catch (mem_out) {
catch (const mem_out &) {
try_reorder();
if (!first) throw;
first = false;
@ -546,7 +546,7 @@ namespace sat {
try {
return bdd(mk_not_rec(b.root), this);
}
catch (mem_out) {
catch (const mem_out &) {
try_reorder();
if (!first) throw;
first = false;
@ -575,7 +575,7 @@ namespace sat {
try {
return bdd(mk_ite_rec(c.root, t.root, e.root), this);
}
catch (mem_out) {
catch (const mem_out &) {
try_reorder();
if (!first) throw;
first = false;

View file

@ -1147,7 +1147,7 @@ namespace sat {
}
}
catch (abort_solver) {
catch (const abort_solver &) {
m_reason_unknown = "sat.giveup";
return l_undef;
}

View file

@ -261,7 +261,7 @@ namespace smt {
try {
for_each_expr(*this, m_visited, n);
}
catch (is_model_value) {
catch (const is_model_value &) {
return true;
}
return false;

View file

@ -177,7 +177,7 @@ namespace smt {
try {
for_each_expr(*this, m_visited, n);
}
catch (is_model_value) {
catch (const is_model_value &) {
return true;
}
return false;
@ -2892,7 +2892,7 @@ namespace smt {
try {
for_each_expr(oc, m_visited, def);
}
catch (occurs) {
catch (const occurs &) {
return false;
}
return true;
@ -2981,7 +2981,7 @@ namespace smt {
try {
process(f);
}
catch (found_satisfied_subset) {
catch (const found_satisfied_subset &) {
set_interp();
copy_non_satisfied(qcandidates, new_qs);
return true;

View file

@ -41,7 +41,7 @@ bool uses_theory(expr * n, family_id fid, expr_mark & visited) {
try {
for_each_expr(p, visited, n);
}
catch (uses_theory_ns::found) {
catch (const uses_theory_ns::found &) {
return true;
}
return false;

View file

@ -89,7 +89,7 @@ bool bv2real_util::contains_bv2real(expr* e) const {
try {
for_each_expr(p, e);
}
catch (contains_bv2real_proc::found) {
catch (const contains_bv2real_proc::found &) {
return true;
}
return false;

View file

@ -226,7 +226,7 @@ class fix_dl_var_tactic : public tactic {
}
return most_occs();
}
catch (failed) {
catch (const failed &) {
return nullptr;
}
}

View file

@ -156,7 +156,7 @@ class lia2pb_tactic : public tactic {
}
return true;
}
catch (failed) {
catch (const failed &) {
return false;
}
}

View file

@ -1034,7 +1034,7 @@ struct is_pb_probe : public probe {
return true;
}
catch (pb2bv_tactic::non_pb) {
catch (const pb2bv_tactic::non_pb &) {
return false;
}
}

View file

@ -371,7 +371,7 @@ class bv1_blaster_tactic : public tactic {
for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, f);
}
}
catch (not_target) {
catch (const not_target &) {
return false;
}
return true;

View file

@ -195,7 +195,7 @@ bool test(goal const & g, Predicate & proc) {
for (unsigned i = 0; i < sz; i++)
quick_for_each_expr(proc, visited, g.form(i));
}
catch (typename Predicate::found) {
catch (const typename Predicate::found &) {
return true;
}
return false;

View file

@ -524,7 +524,7 @@ public:
}
return false;
}
catch (found) {
catch (const found &) {
return true;
}
}
@ -554,7 +554,7 @@ public:
}
return false;
}
catch (found) {
catch (const found &) {
return true;
}
}

View file

@ -870,7 +870,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
m_cache.insert(p);
continue;
}
catch (match_args_aux_proc::no_match) {
catch (const match_args_aux_proc::no_match &) {
return false;
}
}