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

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

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;

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

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

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

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;