mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-15 05:11:49 +00:00
Code Activity

replace some copies with moves

Browse source
This commit is contained in:
Nuno Lopes 2026-02-09 22:45:13 +00:00
parent 73844f9a7f
commit 617c621cc0
8 changed files with 27 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -324,20 +324,20 @@ struct pb2bv_rewriter::imp {
unsigned c = m_coeffs[i].get_unsigned();
v.push_back(c >= k ? k : c);
e.push_back(args[i]);
es.push_back(e);
coeffs.push_back(v);
es.push_back(std::move(e));
coeffs.push_back(std::move(v));
}
while (es.size() > 1) {
for (unsigned i = 0; i + 1 < es.size(); i += 2) {
expr_ref_vector o(m);
unsigned_vector oc;
tot_adder(es[i], coeffs[i], es[i + 1], coeffs[i + 1], k, o, oc);
es[i / 2].set(o);
coeffs[i / 2] = oc;
es[i / 2] = std::move(o);
coeffs[i / 2] = std::move(oc);
}
if ((es.size() % 2) == 1) {
es[es.size() / 2].set(es.back());
coeffs[es.size() / 2] = coeffs.back();
es[es.size() / 2] = std::move(es.back());
coeffs[es.size() / 2] = std::move(coeffs.back());
}
es.shrink((1 + es.size())/2);
coeffs.shrink((1 + coeffs.size())/2);