From 6e09a06307a4ef75195ad005c81bf1d3c62172fc Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 5 Feb 2026 17:15:43 +0000
Subject: [PATCH] Add move semantics to z3::context class

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 examples/c++/test_move_context.cpp | 116 +++++++++++++++++++++++++++++
 examples/c++/test_move_simple.cpp  |  45 +++++++++++
 src/api/c++/z3++.h                 |  18 +++++
 3 files changed, 179 insertions(+)
 create mode 100644 examples/c++/test_move_context.cpp
 create mode 100644 examples/c++/test_move_simple.cpp

diff --git a/examples/c++/test_move_context.cpp b/examples/c++/test_move_context.cpp
new file mode 100644
index 000000000..e220f2708
--- /dev/null
+++ b/examples/c++/test_move_context.cpp
@@ -0,0 +1,116 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Test file for move semantics of z3::context
+--*/
+
+#include <iostream>
+#include <utility>
+#include <cassert>
+#include "z3++.h"
+
+using namespace z3;
+
+// Test move constructor
+void test_move_constructor() {
+    std::cout << "Testing move constructor...\n";
+    
+    context c1;
+    
+    // Move construct c2 from c1
+    context c2(std::move(c1));
+    
+    // c2 should now own the context, and we can use it
+    expr x = c2.int_const("x");
+    solver s(c2);
+    s.add(x > 0);
+    
+    check_result result = s.check();
+    assert(result == sat);
+    
+    std::cout << "Move constructor test passed!\n";
+}
+
+// Test move assignment operator
+void test_move_assignment() {
+    std::cout << "Testing move assignment operator...\n";
+    
+    context c1;
+    
+    context c2;
+    
+    // Move assign c1 to c2
+    c2 = std::move(c1);
+    
+    // c2 should now own c1's context, and we can use it
+    expr x = c2.int_const("x");
+    solver s(c2);
+    s.add(x > 0);
+    
+    check_result result = s.check();
+    assert(result == sat);
+    
+    std::cout << "Move assignment test passed!\n";
+}
+
+// Test moving context into a function
+context create_context_with_config() {
+    context c;
+    c.set("timeout", 5000);
+    return c; // Will use move constructor
+}
+
+void test_return_by_value() {
+    std::cout << "Testing return by value...\n";
+    
+    context c = create_context_with_config();
+    
+    // Use the returned context
+    expr x = c.int_const("x");
+    solver s(c);
+    s.add(x > 0);
+    
+    check_result result = s.check();
+    assert(result == sat);
+    
+    std::cout << "Return by value test passed!\n";
+}
+
+// Test storing context in a container (e.g., vector)
+void test_vector_storage() {
+    std::cout << "Testing vector storage...\n";
+    
+    std::vector<context> contexts;
+    
+    // Create a context and move it into the vector
+    context c;
+    contexts.push_back(std::move(c));
+    
+    // Use the context from the vector
+    expr x = contexts[0].int_const("x");
+    solver s(contexts[0]);
+    s.add(x > 0);
+    
+    check_result result = s.check();
+    assert(result == sat);
+    
+    std::cout << "Vector storage test passed!\n";
+}
+
+int main() {
+    std::cout << "Running z3::context move semantics tests...\n\n";
+    
+    try {
+        test_move_constructor();
+        test_move_assignment();
+        test_return_by_value();
+        test_vector_storage();
+        
+        std::cout << "\nAll tests passed!\n";
+        return 0;
+    }
+    catch (const exception& e) {
+        std::cerr << "Test failed with exception: " << e << "\n";
+        return 1;
+    }
+}
diff --git a/examples/c++/test_move_simple.cpp b/examples/c++/test_move_simple.cpp
new file mode 100644
index 000000000..c5ba0fae7
--- /dev/null
+++ b/examples/c++/test_move_simple.cpp
@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Simple test file for move semantics of z3::context
+--*/
+
+#include <iostream>
+#include <utility>
+#include "z3++.h"
+
+using namespace z3;
+
+int main() {
+    std::cout << "Test 1: Move constructor\n";
+    {
+        context c1;
+        std::cout << "Created c1\n";
+        
+        context c2(std::move(c1));
+        std::cout << "Moved c1 to c2\n";
+        
+        expr x = c2.int_const("x");
+        std::cout << "Created expression in c2\n";
+    }
+    std::cout << "Test 1 passed!\n\n";
+    
+    std::cout << "Test 2: Move assignment\n";
+    {
+        context c1;
+        std::cout << "Created c1\n";
+        
+        context c2;
+        std::cout << "Created c2\n";
+        
+        c2 = std::move(c1);
+        std::cout << "Move assigned c1 to c2\n";
+        
+        expr x = c2.int_const("x");
+        std::cout << "Created expression in c2\n";
+    }
+    std::cout << "Test 2 passed!\n\n";
+    
+    std::cout << "All tests passed!\n";
+    return 0;
+}
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a55918058..55a446ff7 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -214,6 +214,24 @@ namespace z3 {
     public:
         context() { config c; init(c); }
         context(config & c) { init(c); }
+        
+        context(context && other) noexcept 
+            : m_enable_exceptions(other.m_enable_exceptions),
+              m_rounding_mode(other.m_rounding_mode),
+              m_ctx(other.m_ctx) {
+            other.m_ctx = nullptr;
+        }
+        
+        context & operator=(context && other) noexcept {
+            if (this != &other) {
+                if (m_ctx) Z3_del_context(m_ctx);
+                m_enable_exceptions = other.m_enable_exceptions;
+                m_rounding_mode = other.m_rounding_mode;
+                m_ctx = other.m_ctx;
+                other.m_ctx = nullptr;
+            }
+            return *this;
+        }
         ~context() { if (m_ctx) Z3_del_context(m_ctx); }
         operator Z3_context() const { return m_ctx; }