mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 21:01:49 +00:00
Code Activity

Optimize push_back with std::move for std::make_pair in 6 files

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-11 21:39:10 +00:00
parent d68c51f6e7
commit d88c766479
6 changed files with 27 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/pp.cpp
View file

@ -71,7 +71,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
unsigned i;
int space_left;
svector<std::pair<format *, unsigned> > 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;

8
src/ast/rewriter/factor_rewriter.cpp
View file

@ -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)) {

2
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -93,7 +93,7 @@ struct pb2bv_rewriter::imp {
void sort_args() {
vector<ca> 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();

2
src/ast/rewriter/pb_rewriter.cpp
View file

@ -209,7 +209,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
vector<std::pair<expr*,rational> > 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()) {

8
src/smt/theory_array_base.cpp
View file

@ -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)));
}
}
}

20
src/smt/theory_utvpi.cpp
View file

@ -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;
}