From cc7e6cd92dc5965719add9e8b13adffda6a9571d Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 13 Feb 2026 12:16:47 +0000 Subject: [PATCH] Eliminate unnecessary copies with std::move for ref-counted types (#8591) --- src/ackermannization/lackr_model_constructor.cpp | 2 +- src/muz/spacer/spacer_antiunify.cpp | 6 +++--- src/sat/smt/arith_diagnostics.cpp | 2 +- src/sat/smt/q_mbi.cpp | 2 +- src/sat/smt/recfun_solver.cpp | 3 +-- src/smt/dyn_ack.cpp | 2 +- src/smt/smt_parallel.cpp | 2 +- src/smt/theory_recfun.cpp | 5 ++--- src/smt/theory_seq.cpp | 2 +- 9 files changed, 12 insertions(+), 14 deletions(-) diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 63639766f..5a4add54f 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -247,7 +247,7 @@ private: ); m_app2val.insert(a, result.get()); // memoize m_pinned.push_back(a); - m_pinned.push_back(result); + m_pinned.push_back(std::move(result)); return true; } diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp index 1c65b4e29..1fe1529dd 100644 --- a/src/muz/spacer/spacer_antiunify.cpp +++ b/src/muz/spacer/spacer_antiunify.cpp @@ -278,9 +278,9 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m, substitute_vars_by_const(m, au.get_generalization(), const_ref, lit3); expr_ref_vector args(m); - args.push_back(lit1); - args.push_back(lit2); - args.push_back(lit3); + args.push_back(std::move(lit1)); + args.push_back(std::move(lit2)); + args.push_back(std::move(lit3)); expr_ref body_with_consts = mk_and(args); // 3. replace const by var diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 3203bcc4a..7b1d1e80d 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -220,7 +220,7 @@ namespace arith { expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m); if (!is_eq) eq = m.mk_not(eq); args.push_back(arith.mk_int(1)); - args.push_back(eq); + args.push_back(std::move(eq)); }; rational lc(1); for (unsigned i = m_lit_head; i < m_lit_tail; ++i) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index a6eb4910d..41d5b867a 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -430,7 +430,7 @@ namespace q { expr_ref meq = mk_or(meqs); expr_ref veq = mk_or(veqs); assert_expr(meq); - qb.domain_eqs.push_back(veq); + qb.domain_eqs.push_back(std::move(veq)); } } diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index 89688a037..909b673e3 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -139,9 +139,8 @@ namespace recfun { */ void solver::disable_guard(expr* guard, expr_ref_vector const& guards) { SASSERT(!is_enabled_guard(guard)); - app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); expr_ref_vector core(m); - core.push_back(dlimit); + core.push_back(m_util.mk_num_rounds_pred(m_num_rounds)); core.push_back(guard); if (!m_guard2pending.contains(guard)) { m_disabled_guards.push_back(guard); diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 5ac4e884d..3779911cd 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -81,7 +81,7 @@ namespace smt { app * eq = m.mk_eq(arg1, arg2); app_ref neq(m.mk_not(eq), m); if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) { - lits.push_back(neq); + lits.push_back(std::move(neq)); prs.push_back(mk_hypothesis(m, eq, false, arg1, arg2)); } } diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index b2c6bf286..952372120 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -523,7 +523,7 @@ namespace smt { break; expr_ref lit(g2l.to()); lit = g2l(t->get_literal().get()); - cube.push_back(lit); + cube.push_back(std::move(lit)); t = t->parent(); } return true; diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 9f5d54d43..d2dffaf98 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -161,9 +161,8 @@ namespace smt { */ void theory_recfun::disable_guard(expr* guard, expr_ref_vector const& guards) { SASSERT(!is_enabled_guard(guard)); - app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); expr_ref_vector core(m); - core.push_back(dlimit); + core.push_back(m_util.mk_num_rounds_pred(m_num_rounds)); core.push_back(guard); if (!m_guard2pending.contains(guard)) { m_disabled_guards.push_back(guard); @@ -418,7 +417,7 @@ namespace smt { if (u().has_rec_defs() || !m_disabled_guards.empty()) { app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); TRACEFN("add_theory_assumption " << dlimit); - assumptions.push_back(dlimit); + assumptions.push_back(std::move(dlimit)); for (expr* e : m_disabled_guards) assumptions.push_back(m.mk_not(e)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5662edabf..7732bc683 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3350,7 +3350,7 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth); m_trail_stack.push(value_trail(m_max_unfolding_lit)); m_max_unfolding_lit = mk_literal(dlimit); - assumptions.push_back(dlimit); + assumptions.push_back(std::move(dlimit)); for (auto const& kv : m_length_limit_map) { if (kv.m_value > 0) assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value));