z3_4_{8_5,8,11,12}: fix clang-19 build

Original commit message by Reno Dakota (https://github.com/paparodeo),
rebased against latest z3 changes:

z3 contains a bunch of typos in never used functions. The update to
clang-19 now reports the typos -- wrong member function / variable
names.  There is an upstream patch which fixes some of these:

Z3Prover/z3@2ce89e5

And the others we patch or remove as the upstream code has since been
modified.

pkgs/applications/science/logic/z3/4-8-5-typos.diff

@@ -0,0 +1,26 @@
+diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
+index 4c17df2..4c3c311 100644
+--- a/src/util/lp/lp_core_solver_base.h
++++ b/src/util/lp/lp_core_solver_base.h
+@@ -600,8 +600,6 @@ public:
+            out << " \n";
+     }
+
+-    bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }
+-
+     bool column_has_upper_bound(unsigned j) const {
+         switch(m_column_types[j]) {
+         case column_type::free_column:
+diff --git a/src/util/lp/static_matrix_def.h b/src/util/lp/static_matrix_def.h
+index 7949573..2f1cb42 100644
+--- a/src/util/lp/static_matrix_def.h
++++ b/src/util/lp/static_matrix_def.h
+@@ -86,7 +86,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
+     init_row_columns(m, m);
+     while (m--) {
+         for (auto & col : A.m_columns[m]){
+-            set(col.var(), m, A.get_value_of_column_cell(col));
++            set(col.var(), m, A.get_column_cell(col));
+         }
+     }
+ }

pkgs/applications/science/logic/z3/default.nix

@@ -2,6 +2,7 @@
   lib,
   stdenv,
   fetchFromGitHub,
+  fetchpatch,
   python,
   fixDarwinDylibNames,
   javaBindings ? false,
@@ -12,6 +13,7 @@
   findlib ? null,
   zarith ? null,
   writeScript,
+  replaceVars,
 }:
 
 assert javaBindings -> jdk != null;
@@ -123,6 +125,27 @@ let
         ];
       };
     };
+
+  static-matrix-def-patch = fetchpatch {
+    # clang / gcc fixes. fixes typos in some member names
+    name = "gcc-15-fixes.patch";
+    url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch";
+    includes = [ "src/math/lp/static_matrix_def.h" ];
+    hash = "sha256-rEH+UzylzyhBdtx65uf8QYj5xwuXOyG6bV/4jgKkXGo=";
+  };
+
+  static-matrix-patch = fetchpatch {
+    # clang / gcc fixes. fixes typos in some member names
+    name = "gcc-15-fixes.patch";
+    url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch";
+    includes = [ "src/@dir@/lp/static_matrix.h" ];
+    stripLen = 3;
+    extraPrefix = "src/@dir@/";
+    hash = "sha256-+H1/VJPyI0yq4M/61ay8SRCa6OaoJ/5i+I3zVTAPUVo=";
+  };
+
+  # replace @dir@ in the path of the given list of patches
+  fixupPatches = dir: map (patch: replaceVars patch { dir = dir; });
 in
 {
   z3_4_13 = common {
@@ -132,18 +155,53 @@ in
   z3_4_12 = common {
     version = "4.12.6";
     sha256 = "sha256-X4wfPWVSswENV0zXJp/5u9SQwGJWocLKJ/CNv57Bt+E=";
+    patches =
+      fixupPatches "math" [
+        ./lower-bound-typo.diff
+        static-matrix-patch
+      ]
+      ++ [
+        static-matrix-def-patch
+      ];
   };
   z3_4_11 = common {
     version = "4.11.2";
     sha256 = "sha256-OO0wtCvSKwGxnKvu+AfXe4mEzv4nofa7A00BjX+KVjc=";
+    patches =
+      fixupPatches "math" [
+        ./lower-bound-typo.diff
+        static-matrix-patch
+        ./tail-matrix.diff
+      ]
+      ++ [
+        static-matrix-def-patch
+      ];
   };
   z3_4_8 = common {
     version = "4.8.17";
     sha256 = "sha256-BSwjgOU9EgCcm18Zx0P9mnoPc9ZeYsJwEu0ffnACa+8=";
+    patches =
+      fixupPatches "math" [
+        ./lower-bound-typo.diff
+        static-matrix-patch
+        ./tail-matrix.diff
+      ]
+      ++ [
+        static-matrix-def-patch
+      ];
   };
   z3_4_8_5 = common {
     tag = "Z3";
     version = "4.8.5";
     sha256 = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
+    patches =
+      fixupPatches "util" [
+        ./lower-bound-typo.diff
+        static-matrix-patch
+        ./tail-matrix.diff
+      ]
+      ++ [
+        ./4-8-5-typos.diff
+      ];
   };
 }

pkgs/applications/science/logic/z3/lower-bound-typo.diff

@@ -0,0 +1,13 @@
+diff --git a/src/@dir@/lp/column_info.h b/src/@dir@/lp/column_info.h
+index 1dc0c60..9cbeea6 100644
+--- a/src/@dir@/lp/column_info.h
++++ b/src/@dir@/lp/column_info.h
+@@ -47,7 +47,7 @@ public:
+             m_lower_bound_is_strict == c.m_lower_bound_is_strict &&
+             m_upper_bound_is_set == c.m_upper_bound_is_set&&
+             m_upper_bound_is_strict == c.m_upper_bound_is_strict&&
+-            (!m_lower_bound_is_set || m_lower_bound == c.m_low_bound) &&
++            (!m_lower_bound_is_set || m_lower_bound == c.m_lower_bound) &&
+             (!m_upper_bound_is_set || m_upper_bound == c.m_upper_bound) &&
+             m_cost == c.m_cost &&
+             m_is_fixed == c.m_is_fixed &&

pkgs/applications/science/logic/z3/tail-matrix.diff

@@ -0,0 +1,12 @@
+diff --git a/src/@dir@/lp/tail_matrix.h b/src/@dir@/lp/tail_matrix.h
+index 2047e8c..c84340e 100644
+--- a/src/@dir@/lp/tail_matrix.h
++++ b/src/@dir@/lp/tail_matrix.h
+@@ -43,7 +43,6 @@ public:
+         const tail_matrix & m_A;
+         unsigned m_row;
+         ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {}
+-        T operator[](unsigned j) const { return m_A.get_elem(m_row, j);}
+     };
+     ref_row operator[](unsigned i) const { return ref_row(*this, i);}
+ };