From 9ea37793afcc68f8655aae4e69dcda3ae5ec7a04 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 5 Feb 2026 16:57:02 +0000 Subject: [PATCH 1/4] Initial plan 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 2/4] 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 +#include +#include +#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 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 +#include +#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; } From ae88f4e159cca0a1c19685cad2b079f9eeb71417 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 5 Feb 2026 17:16:20 +0000 Subject: [PATCH 3/4] Remove debug test file Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- examples/c++/test_move_simple.cpp | 45 ------------------------------- 1 file changed, 45 deletions(-) delete mode 100644 examples/c++/test_move_simple.cpp diff --git a/examples/c++/test_move_simple.cpp b/examples/c++/test_move_simple.cpp deleted file mode 100644 index c5ba0fae7..000000000 --- a/examples/c++/test_move_simple.cpp +++ /dev/null @@ -1,45 +0,0 @@ -/*++ -Copyright (c) 2026 Microsoft Corporation - -Simple test file for move semantics of z3::context ---*/ - -#include -#include -#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; -} From 7584a282529244c574995202cfd5d859facf4db9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Feb 2026 23:01:47 -0800 Subject: [PATCH 4/4] Delete examples/c++/test_move_context.cpp --- examples/c++/test_move_context.cpp | 116 ----------------------------- 1 file changed, 116 deletions(-) delete mode 100644 examples/c++/test_move_context.cpp diff --git a/examples/c++/test_move_context.cpp b/examples/c++/test_move_context.cpp deleted file mode 100644 index e220f2708..000000000 --- a/examples/c++/test_move_context.cpp +++ /dev/null @@ -1,116 +0,0 @@ -/*++ -Copyright (c) 2026 Microsoft Corporation - -Test file for move semantics of z3::context ---*/ - -#include -#include -#include -#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 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; - } -}