Merge branch 'master' into copilot/update-nightly-build-test-process

src/CMakeLists.txt

@@ -134,6 +134,10 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
     # Enable RPATH support
     MACOSX_RPATH TRUE
   )
+  # Add header padding to allow install_name_tool to modify the dylib
+  # This fixes issues where install_name_tool fails with "larger updated load commands do not fit"
+  # See: https://github.com/Z3Prover/z3/issues/7623
+  target_link_options(libz3 PRIVATE "-Wl,-headerpad_max_install_names")
 endif()
 
 if (NOT MSVC)

src/api/java/CMakeLists.txt

@@ -48,6 +48,10 @@ target_include_directories(z3java PRIVATE
   "${PROJECT_BINARY_DIR}/src/api"
   ${JNI_INCLUDE_DIRS}
 )
+# Add header padding for macOS to allow install_name_tool to modify the dylib
+if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+  target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
+endif()
 # FIXME: Should this library have SONAME and VERSION set?
 
 # On macOS, add headerpad for install_name_tool compatibility

src/api/julia/CMakeLists.txt

@@ -34,6 +34,10 @@ target_include_directories(z3jl PRIVATE
     "${PROJECT_BINARY_DIR}/src/api"
     "${PROJECT_SOURCE_DIR}/src/api/c++"
 )
+# Add header padding for macOS to allow install_name_tool to modify the dylib
+if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+  target_link_options(z3jl PRIVATE "-Wl,-headerpad_max_install_names")
+endif()
 
 # On macOS, add headerpad for install_name_tool compatibility
 if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")

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

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

src/nlsat/nlsat_explain.cpp

@@ -100,8 +100,8 @@ namespace nlsat {
             m_simplify_cores   = false;
             m_full_dimensional = false;
             m_minimize_cores   = false;
-            m_add_all_coeffs   = true;
-            m_add_zero_disc = true;
+            m_add_all_coeffs   = false;
+            m_add_zero_disc    = false;
         }
 
     // display helpers moved to free functions in nlsat_common.h
@@ -901,11 +901,11 @@ namespace nlsat {
             yy = m_pm.mk_polynomial(y);
             p_diff = 2*A*yy + B;
             p_diff = m_pm.normalize(p_diff);
-            int sq = ensure_sign(q); 
+            int sq = ensure_sign_quad(q); 
             if (sq < 0) {
                 return false;
             }
-            int sa = ensure_sign(A);
+            int sa = ensure_sign_quad(A);
             if (sa == 0) {
                 q = B*yy + C;
                 return mk_plinear_root(k, y, i, q);
@@ -918,12 +918,23 @@ namespace nlsat {
             return true;
         }
 
-        int ensure_sign(polynomial_ref & p) {
+        void ensure_sign(polynomial_ref & p) {
+            if (is_const(p) || m_processed.contains(p))
+                return;
             int s = sign(p);
-            if (!is_const(p)) {
+            TRACE(nlsat_explain, tout << p << "\n";);
+            add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
+            // Also add p to the projection to ensure proper cell construction
+            insert_fresh_factors_in_todo(p);
+        }
+
+        // Specialized version for quadratic root handling.
+        // Returns the sign value (-1, 0, or 1).
+        int ensure_sign_quad(polynomial_ref & p) {
+            int s = sign(p);
+            if (!is_const(p) && !m_processed.contains(p)) {
                 TRACE(nlsat_explain, tout << p << "\n";);
                 add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
-                // Also add p to the projection to ensure proper cell construction
                 insert_fresh_factors_in_todo(p);
             }
             return s;
@@ -1101,7 +1112,6 @@ namespace nlsat {
                 use_all_coeffs = true;
             }
             // Set m_add_all_coeffs for the rest of the projection, restore on function exit
-            flet<bool> _set_all_coeffs(m_add_all_coeffs, use_all_coeffs || m_add_all_coeffs);
             
             var x = m_todo.extract_max_polys(ps);
             collect_to_processed(ps);
@@ -1665,6 +1675,7 @@ namespace nlsat {
         void compute_conflict_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
             SASSERT(check_already_added());
             SASSERT(num > 0);
+            flet<bool> _restore_add_all_coeffs(m_add_all_coeffs, false);
             TRACE(nlsat_explain, 
                   tout << "the infeasible clause:\n"; 
                   display(tout, m_solver, num, ls) << "\n";

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

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

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;

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

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() {

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