From df9943568857ce91906c76a17c5d7d440376d1ad Mon Sep 17 00:00:00 2001 From: Morgan Jones Date: Mon, 30 Dec 2024 13:22:37 -0800 Subject: [PATCH] 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: https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b And the others we patch or remove as the upstream code has since been modified. --- .../science/logic/z3/4-8-5-typos.diff | 26 +++++++++ .../applications/science/logic/z3/default.nix | 58 +++++++++++++++++++ .../science/logic/z3/lower-bound-typo.diff | 13 +++++ .../science/logic/z3/tail-matrix.diff | 12 ++++ 4 files changed, 109 insertions(+) create mode 100644 pkgs/applications/science/logic/z3/4-8-5-typos.diff create mode 100644 pkgs/applications/science/logic/z3/lower-bound-typo.diff create mode 100644 pkgs/applications/science/logic/z3/tail-matrix.diff diff --git a/pkgs/applications/science/logic/z3/4-8-5-typos.diff b/pkgs/applications/science/logic/z3/4-8-5-typos.diff new file mode 100644 index 000000000000..64a4887e0ef4 --- /dev/null +++ b/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::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)); + } + } + } diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 91fa924906ac..6e54f4ff4cca 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/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 + ]; }; } diff --git a/pkgs/applications/science/logic/z3/lower-bound-typo.diff b/pkgs/applications/science/logic/z3/lower-bound-typo.diff new file mode 100644 index 000000000000..254c35be5369 --- /dev/null +++ b/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 && diff --git a/pkgs/applications/science/logic/z3/tail-matrix.diff b/pkgs/applications/science/logic/z3/tail-matrix.diff new file mode 100644 index 000000000000..4f680e7617d2 --- /dev/null +++ b/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);} + };