From c0be7ac621d3ea2cc95673b9c81dfcf292de049c Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sun, 8 Feb 2026 18:53:43 +0000
Subject: [PATCH] Remove unused swap() methods (#8538)

---
 src/math/dd/dd_bdd.h         |  2 +-
 src/math/dd/dd_pdd.h         |  2 +-
 src/util/obj_hashtable.h     |  4 ----
 src/util/obj_ref.h           | 11 +++++++----
 src/util/ref_pair_vector.h   |  5 -----
 src/util/scoped_ptr_vector.h |  5 ++---
 src/util/util.h              |  4 ++--
 src/util/vector.h            |  8 ++++----
 8 files changed, 17 insertions(+), 24 deletions(-)

diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h
index 93332bd91..352b48551 100644
--- a/src/math/dd/dd_bdd.h
+++ b/src/math/dd/dd_bdd.h
@@ -278,7 +278,7 @@ namespace dd {
         bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
     public:
         bdd(bdd const & other): root(other.root), m(other.m) { m->inc_ref(root); }
-        bdd(bdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); }
+        bdd(bdd && other) noexcept : root(other.root), m(other.m) { other.root = 0; }
         bdd& operator=(bdd const& other);
         ~bdd() { m->dec_ref(root); }
         bdd lo() const { return bdd(m->lo(root), m); }
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index ecdaf1e69..907176f04 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -418,7 +418,7 @@ namespace dd {
     public:
         pdd(pdd_manager& m): pdd(0, m) { SASSERT(is_zero()); }
         pdd(pdd const& other): pdd(other.root, other.m) { m->inc_ref(root); }
-        pdd(pdd && other) noexcept : pdd(0, other.m) { std::swap(root, other.root); }
+        pdd(pdd && other) noexcept : root(other.root), m(other.m) { other.root = 0; }
         pdd& operator=(pdd const& other);
         pdd& operator=(unsigned k);
         pdd& operator=(rational const& k);
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index cf7cdff05..ae53fbe6d 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -206,10 +206,6 @@ public:
             collisions.push_back(kd.m_key);
         }
     }
-
-    void swap(obj_map & other) noexcept {
-        m_table.swap(other.m_table);
-    }
 };
 
 /**
diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h
index 9ab68676d..0c28752be 100644
--- a/src/util/obj_ref.h
+++ b/src/util/obj_ref.h
@@ -52,8 +52,8 @@ public:
         inc_ref();
     }
 
-    obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) {
-        std::swap(m_obj, other.m_obj);
+    obj_ref(obj_ref && other) noexcept : m_obj(other.m_obj), m_manager(other.m_manager) {
+        other.m_obj = nullptr;
     }
 
     ~obj_ref() { dec_ref(); }
@@ -95,8 +95,11 @@ public:
 
     obj_ref & operator=(obj_ref && n) noexcept {
         SASSERT(&m_manager == &n.m_manager);
-        std::swap(m_obj, n.m_obj);
-        n.reset();
+        if (this != &n) {
+            dec_ref();
+            m_obj = n.m_obj;
+            n.m_obj = nullptr;
+        }
         return *this;
     }
 
diff --git a/src/util/ref_pair_vector.h b/src/util/ref_pair_vector.h
index 1ed708168..3f88cfb85 100644
--- a/src/util/ref_pair_vector.h
+++ b/src/util/ref_pair_vector.h
@@ -193,11 +193,6 @@ public:
     TManager & m() const { 
         return get_manager();
     }
-
-    void swap(ref_pair_vector & other) noexcept {
-        SASSERT(&(this->m_manager) == &(other.m_manager));
-        this->m_nodes.swap(other.m_nodes);
-    }
     
     class element_ref {
         elem_t &       m_ref;
diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h
index 06688eb71..8fe5f91ad 100644
--- a/src/util/scoped_ptr_vector.h
+++ b/src/util/scoped_ptr_vector.h
@@ -31,14 +31,13 @@ public:
     scoped_ptr_vector(scoped_ptr_vector& other) = delete;
     scoped_ptr_vector& operator=(scoped_ptr_vector& other) = delete;
 
-    scoped_ptr_vector(scoped_ptr_vector&& other) noexcept {
-        m_vector.swap(other.m_vector);
+    scoped_ptr_vector(scoped_ptr_vector&& other) noexcept : m_vector(std::move(other.m_vector)) {
     }
     scoped_ptr_vector& operator=(scoped_ptr_vector&& other) noexcept {
         if (this == &other)
             return *this;
         reset();
-        m_vector.swap(other.m_vector);
+        m_vector = std::move(other.m_vector);
         return *this;
     }
 
diff --git a/src/util/util.h b/src/util/util.h
index 4b5af2b52..d580209e9 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -231,8 +231,8 @@ public:
         m_ptr(ptr) {
     }
 
-    scoped_ptr(scoped_ptr &&other) noexcept : m_ptr(nullptr) {
-        std::swap(m_ptr, other.m_ptr);
+    scoped_ptr(scoped_ptr &&other) noexcept : m_ptr(other.m_ptr) {
+        other.m_ptr = nullptr;
     }
 
     ~scoped_ptr() {
diff --git a/src/util/vector.h b/src/util/vector.h
index 8932a789c..b0c1a0b6b 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -165,8 +165,8 @@ public:
         SASSERT(size() == source.size());
     }
 
-    vector(vector&& other) noexcept {
-        std::swap(m_data, other.m_data);
+    vector(vector&& other) noexcept : m_data(other.m_data) {
+        other.m_data = nullptr;
     }
 
     vector(SZ s, T const * data) {
@@ -225,8 +225,8 @@ public:
             return *this;
         }
         destroy();
-        m_data = nullptr;
-        std::swap(m_data, source.m_data);
+        m_data = source.m_data;
+        source.m_data = nullptr;
         return *this;
     }