From d88c766479ba12e9959243d4d4f55c48f3f45185 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 11 Feb 2026 21:39:10 +0000 Subject: [PATCH] Optimize push_back with std::move for std::make_pair in 6 files Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> --- src/ast/pp.cpp | 14 +++++++------- src/ast/rewriter/factor_rewriter.cpp | 8 ++++---- src/ast/rewriter/pb2bv_rewriter.cpp | 2 +- src/ast/rewriter/pb_rewriter.cpp | 2 +- src/smt/theory_array_base.cpp | 8 ++++---- src/smt/theory_utvpi.cpp | 20 ++++++++++---------- 6 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp index 9c4c10c69..7b3dddb2d 100644 --- a/src/ast/pp.cpp +++ b/src/ast/pp.cpp @@ -71,7 +71,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p) unsigned i; int space_left; svector > todo; - todo.push_back(std::make_pair(f, 0)); + todo.push_back(std::move(std::make_pair(f, 0))); app_ref space(mk_string(m, " "), fm(m)); while (!todo.empty()) { if (line >= max_num_lines) @@ -94,28 +94,28 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p) out << f->get_decl()->get_parameter(0).get_symbol(); break; case OP_INDENT: - todo.push_back(std::make_pair(to_app(f->get_arg(0)), + todo.push_back(std::move(std::make_pair(to_app(f->get_arg(0)), std::min(indent + f->get_decl()->get_parameter(0).get_int(), - max_indent))); + max_indent)))); break; case OP_COMPOSE: i = f->get_num_args(); while (i > 0) { --i; - todo.push_back(std::make_pair(to_app(f->get_arg(i)), indent)); + todo.push_back(std::move(std::make_pair(to_app(f->get_arg(i)), indent))); } break; case OP_CHOICE: space_left = std::min(max_width - pos, max_ribbon - pos); if (space_left > 0 && fits(m, to_app(f->get_arg(0)), space_left)) - todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent)); + todo.push_back(std::move(std::make_pair(to_app(f->get_arg(0)), indent))); else - todo.push_back(std::make_pair(to_app(f->get_arg(1)), indent)); + todo.push_back(std::move(std::make_pair(to_app(f->get_arg(1)), indent))); break; case OP_LINE_BREAK: case OP_LINE_BREAK_EXT: if (single_line) { - todo.push_back(std::make_pair(space, indent)); + todo.push_back(std::move(std::make_pair(space, indent))); break; } pos = indent; diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp index 89354b236..33333ce9f 100644 --- a/src/ast/rewriter/factor_rewriter.cpp +++ b/src/ast/rewriter/factor_rewriter.cpp @@ -156,8 +156,8 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) { // m_muls: list of products void factor_rewriter::mk_adds(expr* arg1, expr* arg2) { m_adds.reset(); - m_adds.push_back(std::make_pair(arg1, true)); - m_adds.push_back(std::make_pair(arg2, false)); + m_adds.push_back(std::move(std::make_pair(arg1, true))); + m_adds.push_back(std::move(std::make_pair(arg2, false))); rational k; for (unsigned i = 0; i < m_adds.size();) { bool sign = m_adds[i].second; @@ -173,13 +173,13 @@ void factor_rewriter::mk_adds(expr* arg1, expr* arg2) { if (a().is_add(e) && e->get_num_args() > 0) { m_adds[i].first = e->get_arg(0); for (unsigned j = 1; j < e->get_num_args(); ++j) { - m_adds.push_back(std::make_pair(e->get_arg(j),sign)); + m_adds.push_back(std::move(std::make_pair(e->get_arg(j),sign))); } } else if (a().is_sub(e) && e->get_num_args() > 0) { m_adds[i].first = e->get_arg(0); for (unsigned j = 1; j < e->get_num_args(); ++j) { - m_adds.push_back(std::make_pair(e->get_arg(j),!sign)); + m_adds.push_back(std::move(std::make_pair(e->get_arg(j),!sign))); } } else if (a().is_uminus(e)) { diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 95d06f3a2..e8ff1a15e 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -93,7 +93,7 @@ struct pb2bv_rewriter::imp { void sort_args() { vector cas; for (unsigned i = 0; i < m_args.size(); ++i) { - cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m))); + cas.push_back(std::move(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m)))); } std::sort(cas.begin(), cas.end(), compare_coeffs()); m_coeffs.reset(); diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 4f7de21b0..1d4baf526 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -209,7 +209,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons vector > vec; for (unsigned i = 0; i < num_args; ++i) { - vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i))); + vec.push_back(std::move(std::make_pair(args[i], m_util.get_coeff(f, i)))); } switch(f->get_decl_kind()) { diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 979c55de6..ad516b0ee 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -228,7 +228,7 @@ namespace smt { return false; if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) { TRACE(array, tout << "adding axiom2 to todo queue\n";); - m_axiom2_todo.push_back(std::make_pair(store, select)); + m_axiom2_todo.push_back(std::move(std::make_pair(store, select))); return true; } TRACE(array, tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";); @@ -315,7 +315,7 @@ namespace smt { return false; // axiom was already instantiated if (already_diseq(n1, n2)) return false; - m_extensionality_todo.push_back(std::make_pair(n1, n2)); + m_extensionality_todo.push_back(std::move(std::make_pair(n1, n2))); return true; } @@ -328,7 +328,7 @@ namespace smt { enode * nodes[2] = { a1, a2 }; if (!ctx.add_fingerprint(this, 1, 2, nodes)) return; // axiom was already instantiated - m_congruent_todo.push_back(std::make_pair(a1, a2)); + m_congruent_todo.push_back(std::move(std::make_pair(a1, a2))); } @@ -838,7 +838,7 @@ namespace smt { if (i < num_args) { SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root()); parent_sel_set->insert(sel); - todo.push_back(std::make_pair(parent_root, sel)); + todo.push_back(std::move(std::make_pair(parent_root, sel))); } } } diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp index 2072474b0..e13be88b5 100644 --- a/src/smt/theory_utvpi.cpp +++ b/src/smt/theory_utvpi.cpp @@ -85,14 +85,14 @@ namespace smt { bool utvpi_tester::linearize(expr* e) { m_terms.reset(); - m_terms.push_back(std::make_pair(e, rational(1))); + m_terms.push_back(std::move(std::make_pair(e, rational(1)))); return linearize(); } bool utvpi_tester::linearize(expr* e1, expr* e2) { m_terms.reset(); - m_terms.push_back(std::make_pair(e1, rational(1))); - m_terms.push_back(std::make_pair(e2, rational(-1))); + m_terms.push_back(std::move(std::make_pair(e1, rational(1)))); + m_terms.push_back(std::move(std::make_pair(e2, rational(-1)))); return linearize(); } @@ -109,21 +109,21 @@ namespace smt { m_terms.pop_back(); if (a.is_add(e)) { for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul)); + m_terms.push_back(std::move(std::make_pair(to_app(e)->get_arg(i), mul))); } } else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) { - m_terms.push_back(std::make_pair(e2, mul*num)); + m_terms.push_back(std::move(std::make_pair(e2, mul*num))); } else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) { - m_terms.push_back(std::make_pair(e2, mul*num)); + m_terms.push_back(std::move(std::make_pair(e2, mul*num))); } else if (a.is_sub(e, e1, e2)) { - m_terms.push_back(std::make_pair(e1, mul)); - m_terms.push_back(std::make_pair(e2, -mul)); + m_terms.push_back(std::move(std::make_pair(e1, mul))); + m_terms.push_back(std::move(std::make_pair(e2, -mul))); } else if (a.is_uminus(e, e1)) { - m_terms.push_back(std::make_pair(e1, -mul)); + m_terms.push_back(std::move(std::make_pair(e1, -mul))); } else if (a.is_numeral(e, num)) { m_weight += num*mul; @@ -140,7 +140,7 @@ namespace smt { if (r.is_zero()) { continue; } - m_terms.push_back(std::make_pair(kv.m_key, r)); + m_terms.push_back(std::move(std::make_pair(kv.m_key, r))); if (m_terms.size() > 2) { return false; }