mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 12:51:48 +00:00
Code Activity

Revert incorrect std::move around std::make_pair - make_pair already returns rvalue

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:56:23 +00:00
parent 2d9d91c5cc
commit a2f3d647e1
46 changed files with 105 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -3410,7 +3410,7 @@ bool ast_manager::is_hyper_resolve(
SASSERT(params[i+1].is_int());
unsigned x = static_cast<unsigned>(params[i].get_int());
unsigned y = static_cast<unsigned>(params[i+1].get_int());
positions.push_back(std::move(std::make_pair(x, y)));
positions.push_back(std::make_pair(x, y));
substs.push_back(expr_ref_vector(*this));
++i;
}

2
src/ast/ast_pp_util.cpp
View file

@ -57,7 +57,7 @@ void ast_pp_util::display_decls(std::ostream& out) {
recfun::util u(m);
for (unsigned i = m_rec_decls; i < n; ++i) {
func_decl* f = coll.get_rec_decls()[i];
recfuns.push_back(std::move(std::make_pair(f, u.get_def(f).get_rhs())));
recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
}
if (!recfuns.empty())
ast_smt2_pp_recdefs(out, recfuns, m_env);

2
src/ast/ast_smt2_pp.cpp
View file

@ -538,7 +538,7 @@ class smt2_printer {
m_expr2alias->insert(n, idx);
m_aliased_exprs.push_back(n);
m_aliased_pps.push_back(nf);
m_aliased_lvls_names.push_back(std::move(std::make_pair(lvl, name)));
m_aliased_lvls_names.push_back(std::make_pair(lvl, name));
}
void push_frame(expr * n, bool use_alias) {

2
src/ast/euf/euf_mam.cpp
View file

@ -3025,7 +3025,7 @@ namespace euf {
m_compiler.insert(tree, qa, mp, first_idx, false);
}
DEBUG_CODE(if (first_idx == 0) {
m_trees[lbl_id]->get_patterns().push_back(std::move(std::make_pair(qa, mp)));
m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
ctx.get_trail().push(push_back_trail<std::pair<quantifier*, app*>, false>(m_trees[lbl_id]->get_patterns()));
});
TRACE(trigger_bug, tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););

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::move(std::make_pair(f, 0)));
todo.push_back(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::move(std::make_pair(to_app(f->get_arg(0)),
todo.push_back(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::move(std::make_pair(to_app(f->get_arg(i)), indent)));
todo.push_back(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::move(std::make_pair(to_app(f->get_arg(0)), indent)));
todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent));
else
todo.push_back(std::move(std::make_pair(to_app(f->get_arg(1)), indent)));
todo.push_back(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::move(std::make_pair(space, indent)));
todo.push_back(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::move(std::make_pair(arg1, true)));
m_adds.push_back(std::move(std::make_pair(arg2, false)));
m_adds.push_back(std::make_pair(arg1, true));
m_adds.push_back(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::move(std::make_pair(e->get_arg(j),sign)));
m_adds.push_back(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::move(std::make_pair(e->get_arg(j),!sign)));
m_adds.push_back(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::move(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m))));
cas.push_back(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::move(std::make_pair(args[i], m_util.get_coeff(f, i))));
vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i)));
}
switch(f->get_decl_kind()) {

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

@ -4984,7 +4984,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
all_ranges = true;
unsigned ch = 0, ch2 = 0;
svector<std::pair<unsigned, unsigned>> ranges, ranges1;
ranges.push_back(std::move(std::make_pair(0, u().max_char())));
ranges.push_back(std::make_pair(0, u().max_char()));
auto exclude_range = [&](unsigned lower, unsigned upper) {
SASSERT(lower <= upper);
if (lower == 0) {

6
src/math/dd/dd_pdd.cpp
View file

@ -1985,7 +1985,7 @@ namespace dd {
continue;
}
while (!m.is_val(n)) {
m_nodes.push_back(std::move(std::make_pair(true, n)));
m_nodes.push_back(std::make_pair(true, n));
m_mono.vars.push_back(m.var(n));
n = m.hi(n);
}
@ -2002,14 +2002,14 @@ namespace dd {
unsigned n = m_pdd.root;
auto& m = m_pdd.manager();
while (!m.is_val(n)) {
m_nodes.push_back(std::move(std::make_pair(true, n)));
m_nodes.push_back(std::make_pair(true, n));
m_mono.vars.push_back(m.var(n));
n = m.hi(n);
}
m_mono.coeff = m.val(n);
// if m_pdd is constant and non-zero, the iterator should return a single monomial
if (m_nodes.empty() && !m_mono.coeff.is_zero())
m_nodes.push_back(std::move(std::make_pair(false, n)));
m_nodes.push_back(std::make_pair(false, n));
}
pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }

2
src/math/lp/dioph_eq.cpp
View file

@ -285,7 +285,7 @@ namespace lp {
std::ostream& print_lar_term_L(const std_vector<iv>& t, std::ostream& out) const {
vector<std::pair<mpq, unsigned>> tp;
for (const auto& p : t) {
tp.push_back(std::move(std::make_pair(p.coeff(), p.var())));
tp.push_back(std::make_pair(p.coeff(), p.var()));
}
return print_linear_combination_customized(
tp, [](int j) -> std::string { return "x" + std::to_string(j); }, out);

10
src/math/lp/lar_solver.cpp
View file

@ -957,7 +957,7 @@ namespace lp {
for (auto& [v, c] : coeffs)
if (!is_zero(c))
left_side.push_back(std::move(std::make_pair(c, v)));
left_side.push_back(std::make_pair(c, v));
}
void lar_solver::add_touched_row(unsigned rid) {
@ -2731,8 +2731,8 @@ namespace lp {
bool lar_solver::are_equal(lpvar j, lpvar k) {
vector<std::pair<mpq, lpvar>> coeffs;
coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
coeffs.push_back(std::move(std::make_pair(mpq(-1), k)));
coeffs.push_back(std::make_pair(mpq(1), j));
coeffs.push_back(std::make_pair(mpq(-1), k));
lar_term t(coeffs);
subst_known_terms(&t);
return t.is_empty();
@ -2741,8 +2741,8 @@ namespace lp {
std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j, lpvar k) {
vector<std::pair<mpq, lpvar>> coeffs;
coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
coeffs.push_back(std::move(std::make_pair(mpq(-1), k)));
coeffs.push_back(std::make_pair(mpq(1), j));
coeffs.push_back(std::make_pair(mpq(-1), k));
unsigned ej = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var

2
src/math/lp/nla_core.cpp
View file

@ -774,7 +774,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
unsigned arity = mon.vars().size();
auto it = m.find(arity);
if (it == m.end()) {
it = m.insert(it, std::move(std::make_pair(arity, unsigned_vector())));
it = m.insert(it, std::make_pair(arity, unsigned_vector()));
}
it->second.push_back(mon.var());
}

4
src/math/lp/nla_intervals.cpp
View file

@ -112,7 +112,7 @@ void intervals::add_mul_of_degree_one_to_vector(const nex_mul* e, vector<std::pa
SASSERT((*e)[0].pow() == 1);
const nex *ev = (*e)[0].e();
lpvar j = to_var(ev)->var();
v.push_back(std::move(std::make_pair(e->coeff(), j)));
v.push_back(std::make_pair(e->coeff(), j));
}
void intervals::add_linear_to_vector(const nex* e, vector<std::pair<rational, lpvar>> &v) {
@ -122,7 +122,7 @@ void intervals::add_linear_to_vector(const nex* e, vector<std::pair<rational, lp
add_mul_of_degree_one_to_vector(to_mul(e), v);
break;
case expr_type::VAR:
v.push_back(std::move(std::make_pair(rational(1), to_var(e)->var())));
v.push_back(std::make_pair(rational(1), to_var(e)->var()));
break;
default:
SASSERT(!e->is_sum());

2
src/model/model_macro_solver.cpp
View file

@ -513,7 +513,7 @@ void non_auf_macro_solver::collect_candidates(ptr_vector<quantifier> const& qs,
TRACE(model_finder, tout << "considering macro for: " << f->get_name() << "\n";
m->display(tout); tout << "\n";);
if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_mbqi_force_template)) {
full_macros.insert(f, std::move(std::make_pair(m, q)));
full_macros.insert(f, std::make_pair(m, q));
cond_macros.erase(f);
}
else if (!full_macros.contains(f) && !qi->is_auf())

4
src/muz/base/dl_boogie_proof.cpp
View file

@ -107,7 +107,7 @@ namespace datalog {
for (unsigned k = 1; k < premises1.size(); ++k) {
if (m.get_fact(premises1[k].get()) == lit) {
premises2.push_back(premises1[k].get());
positions2.push_back(std::move(std::make_pair(j+1,0)));
positions2.push_back(std::make_pair(j+1,0));
substs2.push_back(expr_ref_vector(m));
break;
}
@ -220,7 +220,7 @@ namespace datalog {
unsigned sz = sub.size();
SASSERT(sz == q->get_num_decls());
for (unsigned i = 0; i < sz; ++i) {
s.push_back(std::move(std::make_pair(q->get_decl_name(sz-1-i), sub[i])));
s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i]));
}
return;
}

4
src/muz/base/dl_util.cpp
View file

@ -334,7 +334,7 @@ namespace datalog {
proof_ref_vector premises(m);
premises.push_back(m.mk_asserted(fml1));
premises.push_back(m.mk_asserted(fml2));
positions.push_back(std::move(std::make_pair(idx+1, 0)));
positions.push_back(std::make_pair(idx+1, 0));
TRACE(dl,
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
@ -372,7 +372,7 @@ namespace datalog {
proof_ref_vector premises(m);
premises.push_back(r1.get_proof());
premises.push_back(r2.get_proof());
positions.push_back(std::move(std::make_pair(idx+1, 0)));
positions.push_back(std::make_pair(idx+1, 0));
TRACE(dl,
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";

8
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -319,7 +319,7 @@ namespace datalog {
}
proof* premises[2] = { pr, p };
positions.push_back(std::move(std::make_pair(0, 1)));
positions.push_back(std::make_pair(0, 1));
substs.push_back(sub1);
substs.push_back(sub);
@ -547,7 +547,7 @@ namespace datalog {
app* body_j = r->get_tail(j);
prop_body = vs(body_j, sub.size(), sub.data());
prs.push_back(get_proof(md, head_j, to_app(prop_body), level-1));
positions.push_back(std::move(std::make_pair(j+1,0)));
positions.push_back(std::make_pair(j+1,0));
substs.push_back(expr_ref_vector(m));
}
pr = m.mk_hyper_resolve(sz+1, prs.data(), prop, positions, substs);
@ -1082,7 +1082,7 @@ namespace datalog {
}
prs.push_back(get_proof(md, to_app(trace->get_arg(j)), path1));
positions.push_back(std::move(std::make_pair(j+1,0)));
positions.push_back(std::make_pair(j+1,0));
substs.push_back(expr_ref_vector(m));
}
head = rl->get_head();
@ -1256,7 +1256,7 @@ namespace datalog {
scoped_proof _sp(m);
proof* premises[2] = { pr, p };
positions.push_back(std::move(std::make_pair(0, 1)));
positions.push_back(std::make_pair(0, 1));
substs.push_back(sub1);
substs.push_back(sub);

8
src/muz/rel/dl_bound_relation.cpp
View file

@ -534,10 +534,10 @@ namespace datalog {
}
uint_set2& src = (*m_elems)[j];
for (unsigned idx : src.lt) {
m_todo.push_back(std::move(std::make_pair(idx, true)));
m_todo.push_back(std::make_pair(idx, true));
}
for (unsigned idx : src.le) {
m_todo.push_back(std::move(std::make_pair(idx, strict)));
m_todo.push_back(std::make_pair(idx, strict));
}
if (strict) {
dst.lt.insert(j);
@ -551,14 +551,14 @@ namespace datalog {
void bound_relation::mk_lt(unsigned i, unsigned j) {
m_todo.reset();
i = find(i);
m_todo.push_back(std::move(std::make_pair(find(j), true)));
m_todo.push_back(std::make_pair(find(j), true));
mk_lt(i);
}
void bound_relation::mk_le(unsigned i, unsigned j) {
m_todo.reset();
i = find(i);
m_todo.push_back(std::move(std::make_pair(find(j), false)));
m_todo.push_back(std::make_pair(find(j), false));
mk_lt(i);
}

2
src/muz/rel/dl_instruction.cpp
View file

@ -76,7 +76,7 @@ namespace datalog {
for(unsigned i = 0; i < n; ++i) {
unsigned sz = reg(i) ? reg(i)->get_size_estimate_bytes() : 0;
total_bytes += sz;
sizes.push_back(std::move(std::make_pair(i, sz)));
sizes.push_back(std::make_pair(i, sz));
}
std::sort(sizes.begin(), sizes.end(), compare_size_proc());

4
src/muz/rel/dl_product_relation.cpp
View file

@ -896,10 +896,10 @@ namespace datalog {
for (unsigned j = i + 1; j < r.size(); ++j) {
relation_mutator_fn& m2 = *(m_mutators[j]);
if (m1.supports_attachment(r[j])) {
m_attach.push_back(std::move(std::make_pair(i,j)));
m_attach.push_back(std::make_pair(i,j));
}
if (m2.supports_attachment(r[i])) {
m_attach.push_back(std::move(std::make_pair(j,i)));
m_attach.push_back(std::make_pair(j,i));
}
}
}

2
src/muz/rel/rel_context.cpp
View file

@ -547,7 +547,7 @@ namespace datalog {
get_rmanager().reset_saturated_marks();
get_relation(pred).add_fact(fact);
if (!m_context.print_aig().is_null()) {
m_table_facts.push_back(std::move(std::make_pair(pred, fact)));
m_table_facts.push_back(std::make_pair(pred, fact));
}
}

2
src/muz/spacer/spacer_sat_answer.cpp
View file

@ -187,7 +187,7 @@ proof *ground_sat_answer_op::mk_proof_step(frame &fr) {
for (auto &k : fr.m_kids) {premises.push_back(m_cache.find(k));}
for (unsigned i = 0; i < premises.size(); ++i) {
positions.push_back(std::move(std::make_pair(0,i)));
positions.push_back(std::make_pair(0,i));
}
for (unsigned i = 0; i <= premises.size(); ++i) {
substs.push_back(expr_ref_vector(m));

6
src/muz/spacer/spacer_sym_mux.cpp
View file

@ -54,14 +54,14 @@ void sym_mux::register_decl(func_decl *fdecl) {
entry->m_variants.push_back(mk_variant(fdecl, 1));
m_entries.insert(fdecl, entry);
m_muxes.insert(entry->m_variants.get(0), std::move(std::make_pair(entry, 0)));
m_muxes.insert(entry->m_variants.get(1), std::move(std::make_pair(entry, 1)));
m_muxes.insert(entry->m_variants.get(0), std::make_pair(entry, 0));
m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1));
}
void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) const {
while (entry.m_variants.size() < sz) {
unsigned idx = entry.m_variants.size();
entry.m_variants.push_back (mk_variant(entry.m_main, idx));
m_muxes.insert(entry.m_variants.back(), std::move(std::make_pair(&entry, idx)));
m_muxes.insert(entry.m_variants.back(), std::make_pair(&entry, idx));
}
}

12
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -154,7 +154,7 @@ namespace spacer {
if (m_ctx.is_b_pure (premise)) {
if (!m_use_constant_from_a) {
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
}
}
else {
@ -163,14 +163,14 @@ namespace spacer {
if (m_use_constant_from_a) {
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
}
}
}
else {
if (m_use_constant_from_a) {
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
}
}
}
@ -199,7 +199,7 @@ namespace spacer {
brw.mk_not(premise, negatedPremise);
pinned.push_back(negatedPremise);
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), to_app(negatedPremise))));
coeff_lits.push_back(std::make_pair(abs(coefficient), to_app(negatedPremise)));
}
}
}
@ -341,7 +341,7 @@ namespace spacer {
coeff_lits_t coeff_lits;
for (unsigned l = 0; l < matrix.num_cols(); ++l) {
if (!matrix.get(k,l).is_zero()) {
coeff_lits.push_back(std::move(std::make_pair(matrix.get(k, l), ordered_basis[l])));
coeff_lits.push_back(std::make_pair(matrix.get(k, l), ordered_basis[l]));
}
}
SASSERT(!coeff_lits.empty());
@ -472,7 +472,7 @@ namespace spacer {
evaluation = (*model)(bounded_vectors[j][k].get());
if (!util.is_zero(evaluation)) {
coeff_lits.push_back(std::move(std::make_pair(rational(1), ordered_basis[j])));
coeff_lits.push_back(std::make_pair(rational(1), ordered_basis[j]));
}
}
SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already

2
src/muz/tab/tab_context.cpp
View file

@ -1623,7 +1623,7 @@ namespace datalog {
proof_ref_vector premises(m);
premises.push_back(m.mk_asserted(r1.to_formula()));
premises.push_back(m.mk_asserted(r2.to_formula()));
positions.push_back(std::move(std::make_pair(idx+1, 0)));
positions.push_back(std::make_pair(idx+1, 0));
pr = m.mk_hyper_resolve(2, premises.data(), fml, positions, substs);
pc.insert(pr);
}

4
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -119,7 +119,7 @@ namespace datalog {
if (a1->get_decl() == a2->get_decl() &&
a1->get_num_args() == a2->get_num_args()) {
for (unsigned k = 0; k < a1->get_num_args(); ++k) {
todo.push_back(std::move(std::make_pair(a1->get_arg(k), a2->get_arg(k))));
todo.push_back(std::make_pair(a1->get_arg(k), a2->get_arg(k)));
}
match(i, pat, j + 1, todo, q, conjs);
todo.resize(sz);
@ -140,7 +140,7 @@ namespace datalog {
if (m_funs.find(to_app(arg)->get_decl(), terms)) {
for (unsigned k = 0; k < terms->size(); ++k) {
todo.push_back(std::move(std::make_pair(arg, (*terms)[k])));
todo.push_back(std::make_pair(arg, (*terms)[k]));
match(i + 1, pat, j, todo, q, conjs);
todo.pop_back();
}

2
src/opt/totalizer.cpp
View file

@ -75,7 +75,7 @@ namespace opt {
m_clauses.push_back(mk_or(clause));
}
def = mk_not(m, mk_and(ors));
m_defs.push_back(std::move(std::make_pair(c, def)));
m_defs.push_back(std::make_pair(c, def));
}
}

2
src/sat/smt/arith_axioms.cpp
View file

@ -578,7 +578,7 @@ namespace arith {
TRACE(artih, tout << mk_bounded_pp(e.eq()->get_expr(), m) << "\n");
ensure_column(e.v1());
ensure_column(e.v2());
m_delayed_eqs.push_back(std::move(std::make_pair(e, false)));
m_delayed_eqs.push_back(std::make_pair(e, false));
ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
}

2
src/sat/smt/arith_internalize.cpp
View file

@ -557,7 +557,7 @@ namespace arith {
rational const& r = m_columns[var];
if (!r.is_zero()) {
auto vi = register_theory_var_in_lar_solver(var);
m_left_side.push_back(std::move(std::make_pair(r, vi)));
m_left_side.push_back(std::make_pair(r, vi));
m_columns[var].reset();
}
}

4
src/sat/smt/arith_solver.cpp
View file

@ -1083,7 +1083,7 @@ namespace arith {
m_nla->am().set(r, m_nla->am_value(t));
}
else {
m_todo_terms.push_back(std::move(std::make_pair(t, rational::one())));
m_todo_terms.push_back(std::make_pair(t, rational::one()));
TRACE(nl_value, tout << "v" << v << " " << t << "\n";);
TRACE(nl_value, tout << "v" << v << " := w" << t << "\n";
lp().print_term(lp().get_term(t), tout) << "\n";);
@ -1103,7 +1103,7 @@ namespace arith {
auto wi = arg.j();
c1 = arg.coeff() * wcoeff;
if (lp().column_has_term(wi)) {
m_todo_terms.push_back(std::move(std::make_pair(wi, c1)));
m_todo_terms.push_back(std::make_pair(wi, c1));
}
else {
m_nla->am().set(r1, c1.to_mpq());

2
src/sat/smt/array_model.cpp
View file

@ -237,7 +237,7 @@ namespace array {
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::move(std::make_pair(parent_root, sel)));
todo.push_back(std::make_pair(parent_root, sel));
}
}
}

2
src/sat/smt/bv_solver.cpp
View file

@ -631,7 +631,7 @@ namespace bv {
bool ok = true;
svector<std::pair<expr*, internalize_mode>> delay;
for (auto kv : m_delay_internalize)
delay.push_back(std::move(std::make_pair(kv.m_key, kv.m_value)));
delay.push_back(std::make_pair(kv.m_key, kv.m_value));
flet<bool> _cheap1(m_cheap_axioms, true);
for (auto [e, mode] : delay)
if (!check_delay_internalized(e))

4
src/sat/smt/dt_solver.cpp
View file

@ -93,8 +93,8 @@ namespace dt {
}
void solver::oc_push_stack(enode* n) {
m_dfs.push_back(std::move(std::make_pair(EXIT, n)));
m_dfs.push_back(std::move(std::make_pair(ENTER, n)));
m_dfs.push_back(std::make_pair(EXIT, n));
m_dfs.push_back(std::make_pair(ENTER, n));
}
/**

18
src/sat/smt/euf_relevancy.cpp
View file

@ -91,7 +91,7 @@ namespace euf {
unsigned sz = m_clauses.size();
m_clauses.push_back(cl);
m_roots.push_back(true);
m_trail.push_back(std::move(std::make_pair(update::add_clause, 0)));
m_trail.push_back(std::make_pair(update::add_clause, 0));
for (sat::literal lit : *cl) {
ctx.s().set_external(lit.var());
occurs(lit).push_back(sz);
@ -113,7 +113,7 @@ namespace euf {
unsigned sz = m_clauses.size();
m_clauses.push_back(cl);
m_roots.push_back(false);
m_trail.push_back(std::move(std::make_pair(update::add_clause, 0)));
m_trail.push_back(std::make_pair(update::add_clause, 0));
for (sat::literal lit : *cl) {
ctx.s().set_external(lit.var());
occurs(lit).push_back(sz);
@ -121,8 +121,8 @@ namespace euf {
}
void relevancy::add_to_propagation_queue(sat::literal lit) {
m_trail.push_back(std::move(std::make_pair(update::add_queue, lit.var())));
m_queue.push_back(std::move(std::make_pair(lit, nullptr)));
m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
m_queue.push_back(std::make_pair(lit, nullptr));
}
void relevancy::set_relevant(sat::literal lit) {
@ -130,7 +130,7 @@ namespace euf {
if (n)
mark_relevant(n);
m_relevant_var_ids.setx(lit.var(), true, false);
m_trail.push_back(std::move(std::make_pair(update::relevant_var, lit.var())));
m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
}
void relevancy::set_asserted(sat::literal lit) {
@ -197,7 +197,7 @@ namespace euf {
flush();
if (m_qhead == m_queue.size())
return;
m_trail.push_back(std::move(std::make_pair(update::set_qhead, m_qhead)));
m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
auto const& [lit, n] = m_queue[m_qhead++];
SASSERT(n || lit != sat::null_literal);
@ -224,8 +224,8 @@ namespace euf {
if (is_relevant(n))
return;
TRACE(relevancy, tout << "mark #" << ctx.bpp(n) << "\n");
m_trail.push_back(std::move(std::make_pair(update::add_queue, 0)));
m_queue.push_back(std::move(std::make_pair(sat::null_literal, n)));
m_trail.push_back(std::make_pair(update::add_queue, 0));
m_queue.push_back(std::make_pair(sat::null_literal, n));
}
void relevancy::mark_relevant(sat::literal lit) {
@ -272,7 +272,7 @@ namespace euf {
if (true_lit != sat::null_literal)
set_asserted(true_lit);
else {
m_trail.push_back(std::move(std::make_pair(update::set_root, idx)));
m_trail.push_back(std::make_pair(update::set_root, idx));
m_roots[idx] = true;
}
next:

2
src/sat/smt/pb_internalize.cpp
View file

@ -82,7 +82,7 @@ namespace pb {
for (unsigned i = 0; i < lits.size(); ++i) {
rational c = m_pb.get_coeff(t, i);
check_unsigned(c);
wlits.push_back(std::move(std::make_pair(c.get_unsigned(), lits[i])));
wlits.push_back(std::make_pair(c.get_unsigned(), lits[i]));
}
}

2
src/sat/smt/q_mbi.cpp
View file

@ -521,7 +521,7 @@ namespace q {
unsigned i = 0;
for (expr* arg : *to_app(s)) {
if (!is_ground(arg) && !is_uninterp(arg) && !qb.is_free(arg))
qb.var_args.push_back(std::move(std::make_pair(to_app(s), i)));
qb.var_args.push_back(std::make_pair(to_app(s), i));
++i;
}
}

4
src/smt/expr_context_simplifier.cpp
View file

@ -428,7 +428,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
done:
if (r) {
cache.insert(e, std::move(std::make_pair(pos, r)));
cache.insert(e, std::make_pair(pos, r));
}
TRACE(expr_context_simplifier,
@ -704,7 +704,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
done:
if (r) {
cache.insert(e, std::move(std::make_pair(pos, r)));
cache.insert(e, std::make_pair(pos, r));
}
TRACE(expr_context_simplifier,

2
src/smt/seq_eq_solver.cpp
View file

@ -1157,7 +1157,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const&
return false;
m.inc_ref(rhs);
m.inc_ref(ls[0]);
m_nth_eq2_cache.insert(std::move(std::make_pair(rhs, ls[0])));
m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
get_trail_stack().push(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
ls1.push_back(s);
if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));

6
src/smt/smt_context.cpp
View file

@ -3238,14 +3238,14 @@ namespace smt {
void context::internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy) {
for (expr* e : asms) {
if (is_valid_assumption(m, e)) {
asm2proxy.push_back(std::move(std::make_pair(e, expr_ref(e, m))));
asm2proxy.push_back(std::make_pair(e, expr_ref(e, m)));
}
else {
expr_ref proxy(m), fml(m);
proxy = m.mk_fresh_const(symbol(), m.mk_bool_sort());
fml = m.mk_implies(proxy, e);
m_asserted_formulas.assert_expr(fml);
asm2proxy.push_back(std::move(std::make_pair(e, proxy)));
asm2proxy.push_back(std::make_pair(e, proxy));
}
}
// The new assertions are of the form 'proxy => assumption'
@ -3332,7 +3332,7 @@ namespace smt {
}
clausep = clause::mk(m, lits.size(), lits.data(), CLS_AUX, js);
}
m_tmp_clauses.push_back(std::move(std::make_pair(clausep, lits)));
m_tmp_clauses.push_back(std::make_pair(clausep, lits));
}
void context::reset_tmp_clauses() {

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::move(std::make_pair(store, select)));
m_axiom2_todo.push_back(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::move(std::make_pair(n1, n2)));
m_extensionality_todo.push_back(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::move(std::make_pair(a1, a2)));
m_congruent_todo.push_back(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::move(std::make_pair(parent_root, sel)));
todo.push_back(std::make_pair(parent_root, sel));
}
}
}

2
src/smt/theory_bv.cpp
View file

@ -1210,7 +1210,7 @@ namespace smt {
}
m_diseq_watch.reserve(watch_var+1);
m_diseq_watch[watch_var].push_back(std::move(std::make_pair(v1, v2)));
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
return;
}

4
src/smt/theory_datatype.cpp
View file

@ -71,8 +71,8 @@ namespace smt {
}
void theory_datatype::oc_push_stack(enode * n) {
m_stack.push_back(std::move(std::make_pair(EXIT, n)));
m_stack.push_back(std::move(std::make_pair(ENTER, n)));
m_stack.push_back(std::make_pair(EXIT, n));
m_stack.push_back(std::make_pair(ENTER, n));
}

2
src/smt/theory_pb.cpp
View file

@ -531,7 +531,7 @@ namespace smt {
case l_false:
break;
default:
args.push_back(std::move(std::make_pair(l, c)));
args.push_back(std::make_pair(l, c));
break;
}
}

2
src/smt/theory_special_relations.cpp
View file

@ -1166,7 +1166,7 @@ namespace smt {
relation& r = *kv.m_value;
if (r.m_property != sr_po) continue;
for (atom* ap : r.m_asserted_atoms) {
atoms.push_back(std::move(std::make_pair(ap->var(), ap->phase())));
atoms.push_back(std::make_pair(ap->var(), ap->phase()));
}
}
}

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::move(std::make_pair(e, rational(1))));
m_terms.push_back(std::make_pair(e, rational(1)));
return linearize();
}
bool utvpi_tester::linearize(expr* e1, expr* e2) {
m_terms.reset();
m_terms.push_back(std::move(std::make_pair(e1, rational(1))));
m_terms.push_back(std::move(std::make_pair(e2, rational(-1))));
m_terms.push_back(std::make_pair(e1, rational(1)));
m_terms.push_back(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::move(std::make_pair(to_app(e)->get_arg(i), mul)));
m_terms.push_back(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::move(std::make_pair(e2, mul*num)));
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
m_terms.push_back(std::move(std::make_pair(e2, mul*num)));
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_sub(e, e1, e2)) {
m_terms.push_back(std::move(std::make_pair(e1, mul)));
m_terms.push_back(std::move(std::make_pair(e2, -mul)));
m_terms.push_back(std::make_pair(e1, mul));
m_terms.push_back(std::make_pair(e2, -mul));
}
else if (a.is_uminus(e, e1)) {
m_terms.push_back(std::move(std::make_pair(e1, -mul)));
m_terms.push_back(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::move(std::make_pair(kv.m_key, r)));
m_terms.push_back(std::make_pair(kv.m_key, r));
if (m_terms.size() > 2) {
return false;
}