From 811f38cfd12b64b938fd7ac0bd417da89db9a64b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 8 Feb 2026 19:02:20 +0000 Subject: [PATCH] Replace user-defined swap with move semantics in multiple files Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> --- src/math/polynomial/polynomial.cpp | 2 +- src/math/polynomial/upolynomial.cpp | 12 ++++++------ src/nlsat/nlsat_scoped_literal_vector.h | 22 ++++++++++++++++++++++ src/qe/nlqsat.cpp | 2 +- src/smt/proto_model/proto_model.cpp | 2 +- src/util/s_integer.cpp | 2 +- 6 files changed, 32 insertions(+), 10 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 2db2e1bb0..111b255f8 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -2134,7 +2134,7 @@ namespace polynomial { m_m2pos.reset(m); m_m2pos.set(m, i); } - m_tmp_as.swap(new_as); + m_tmp_as = std::move(new_as); } // For each monomial m diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 2cf2a7b4e..b11b1ecde 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -249,7 +249,7 @@ namespace upolynomial { void core_manager::neg(unsigned sz, numeral const * p, numeral_vector & buffer) { neg_core(sz, p, m_basic_tmp); - buffer.swap(m_basic_tmp); + buffer = std::move(m_basic_tmp); } // buffer := p1 + p2 @@ -274,7 +274,7 @@ namespace upolynomial { void core_manager::add(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) { add_core(sz1, p1, sz2, p2, m_basic_tmp); - buffer.swap(m_basic_tmp); + buffer = std::move(m_basic_tmp); } // buffer := p1 - p2 @@ -301,7 +301,7 @@ namespace upolynomial { void core_manager::sub(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) { sub_core(sz1, p1, sz2, p2, m_basic_tmp); - buffer.swap(m_basic_tmp); + buffer = std::move(m_basic_tmp); } // buffer := p1 * p2 @@ -342,7 +342,7 @@ namespace upolynomial { void core_manager::mul(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) { mul_core(sz1, p1, sz2, p2, m_basic_tmp); - buffer.swap(m_basic_tmp); + buffer = std::move(m_basic_tmp); } // buffer := dp/dx @@ -800,7 +800,7 @@ namespace upolynomial { TRACE(mgcd, tout << "found GCD\n";); mul(candidate, c_g); flip_sign_if_lm_neg(candidate); - candidate.swap(result); + result = std::move(candidate); TRACE(mgcd, tout << "r: "; display_star(tout, result); tout << "\n";); return; } @@ -1007,7 +1007,7 @@ namespace upolynomial { set(sz, p, result); for (unsigned i = 1; i < k; ++i) mul(m_pw_tmp.size(), m_pw_tmp.data(), sz, p, m_pw_tmp); - r.swap(result); + r = std::move(result); #if 0 unsigned mask = 1; numeral_vector & p2 = m_pw_tmp; diff --git a/src/nlsat/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h index 63c0b2df7..7c31aee15 100644 --- a/src/nlsat/nlsat_scoped_literal_vector.h +++ b/src/nlsat/nlsat_scoped_literal_vector.h @@ -29,6 +29,28 @@ namespace nlsat { public: scoped_literal_vector(solver & s):m_solver(s) {} ~scoped_literal_vector() { reset(); } + + // Move constructor + scoped_literal_vector(scoped_literal_vector && other) noexcept + : m_solver(other.m_solver), m_lits(std::move(other.m_lits)) { + // other.m_lits is now empty, so its destructor won't dec_ref anything + } + + // Move assignment operator + scoped_literal_vector & operator=(scoped_literal_vector && other) noexcept { + if (this != &other) { + SASSERT(&m_solver == &other.m_solver); + reset(); // dec_ref our current literals + m_lits = std::move(other.m_lits); // take ownership of other's literals + // other.m_lits is now empty + } + return *this; + } + + // Delete copy operations to prevent accidental copies + scoped_literal_vector(scoped_literal_vector const &) = delete; + scoped_literal_vector & operator=(scoped_literal_vector const &) = delete; + unsigned size() const { return m_lits.size(); } bool empty() const { return m_lits.empty(); } literal operator[](unsigned i) const { return m_lits[i]; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 1761af08b..6cc6a33c2 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -388,7 +388,7 @@ namespace qe { new_result.reset(); ex.project(vars[i], result.size(), result.data(), new_result); TRACE(qe, display_project(tout, vars[i], result, new_result);); - result.swap(new_result); + result = std::move(new_result); } negate_clause(result); } diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 2d97c4522..a62e51603 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -239,7 +239,7 @@ void proto_model::cleanup() { unregister_decl(faux); } } - m_aux_decls.swap(found_aux_fs); + m_aux_decls = std::move(found_aux_fs); } TRACE(model_bug, model_v2_pp(tout, *this);); } diff --git a/src/util/s_integer.cpp b/src/util/s_integer.cpp index e76781388..53d19270b 100644 --- a/src/util/s_integer.cpp +++ b/src/util/s_integer.cpp @@ -52,7 +52,7 @@ s_integer gcd(const s_integer & r1, const s_integer & r2) { tmp2.neg(); } if (tmp1 < tmp2) { - tmp1.swap(tmp2); + std::swap(tmp1, tmp2); } for(;;) { s_integer aux = tmp1 % tmp2;