mirror of
https://git.freebsd.org/ports.git
synced 2025-04-28 09:36:41 -04:00
math/z3: fix build with clang 19
Clang 19 has become more strict about errors in member functions, which
results in:
/wrkdirs/usr/ports/math/z3/work/z3-z3-4.13.0/src/math/lp/static_matrix.h:82:72: error: no member named 'get' in 'static_matrix<T, X>'; did you mean 'set'?
82 | ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get(v.m_row, v.m_col)); return *this; }
| ^~~
| set
/wrkdirs/usr/ports/math/z3/work/z3-z3-4.13.0/src/math/lp/static_matrix.h:164:10: note: 'set' declared here
164 | void set(unsigned row, unsigned col, T const & val);
| ^
Upstream fixed this as part of a few other changes for gcc 15 in
<https://github.com/Z3Prover/z3/commit/2ce89e5f4>, but it does not apply
cleanly to this version, so add a backported patch.
PR: 281512
MFH: 2024Q3
(cherry picked from commit 88af7aa2d0)
This commit is contained in:
Dimitry Andric
Gleb Popov
parent
59790923d5
commit
1168d8b849
1 changed files with 125 additions and 0 deletions
125
math/z3/files/patch-backport-2ce89e5f4
Normal file
125
math/z3/files/patch-backport-2ce89e5f4
Normal file
|
|
@ -0,0 +1,125 @@
|
|||
From 2ce89e5f491fa817d02d8fdce8c62798beab258b Mon Sep 17 00:00:00 2001
|
||||
From: David Seifert <16636962+SoapGentoo@users.noreply.github.com>
|
||||
Date: Mon, 29 Jul 2024 20:07:10 +0200
|
||||
Subject: [PATCH] Gcc 15 two phase (#7313)
|
||||
|
||||
* Fix `-Wclass-memaccess`
|
||||
|
||||
* Fix for GCC 15 two-phase lookup
|
||||
|
||||
* GCC 15 is more aggressive about checking dependent names:
|
||||
https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=r15-2117-g313afcfdabeab3
|
||||
|
||||
Bug: https://bugs.gentoo.org/936634
|
||||
---
|
||||
src/math/lp/lp_settings.h | 69 ++++++++++++++++-----------------
|
||||
src/math/lp/static_matrix.h | 2 +-
|
||||
src/math/lp/static_matrix_def.h | 2 +-
|
||||
3 files changed, 36 insertions(+), 37 deletions(-)
|
||||
|
||||
diff --git src/math/lp/lp_settings.h src/math/lp/lp_settings.h
|
||||
index d1a4be21c64..0d47877c76b 100644
|
||||
--- src/math/lp/lp_settings.h
|
||||
+++ src/math/lp/lp_settings.h
|
||||
--- src/math/lp/lp_settings.h.orig 2024-03-07 18:25:16 UTC
|
||||
+++ src/math/lp/lp_settings.h
|
||||
@@ -97,39 +97,39 @@ struct statistics {
|
||||
};
|
||||
|
||||
struct statistics {
|
||||
- unsigned m_make_feasible;
|
||||
- unsigned m_total_iterations;
|
||||
- unsigned m_iters_with_no_cost_growing;
|
||||
- unsigned m_num_factorizations;
|
||||
- unsigned m_num_of_implied_bounds;
|
||||
- unsigned m_need_to_solve_inf;
|
||||
- unsigned m_max_cols;
|
||||
- unsigned m_max_rows;
|
||||
- unsigned m_gcd_calls;
|
||||
- unsigned m_gcd_conflicts;
|
||||
- unsigned m_cube_calls;
|
||||
- unsigned m_cube_success;
|
||||
- unsigned m_patches;
|
||||
- unsigned m_patches_success;
|
||||
- unsigned m_hnf_cutter_calls;
|
||||
- unsigned m_hnf_cuts;
|
||||
- unsigned m_nla_calls;
|
||||
- unsigned m_gomory_cuts;
|
||||
- unsigned m_nla_add_bounds;
|
||||
- unsigned m_nla_propagate_bounds;
|
||||
- unsigned m_nla_propagate_eq;
|
||||
- unsigned m_nla_lemmas;
|
||||
- unsigned m_nra_calls;
|
||||
- unsigned m_nla_bounds_improvements;
|
||||
- unsigned m_horner_calls;
|
||||
- unsigned m_horner_conflicts;
|
||||
- unsigned m_cross_nested_forms;
|
||||
- unsigned m_grobner_calls;
|
||||
- unsigned m_grobner_conflicts;
|
||||
- unsigned m_offset_eqs;
|
||||
- unsigned m_fixed_eqs;
|
||||
+ unsigned m_make_feasible = 0;
|
||||
+ unsigned m_total_iterations = 0;
|
||||
+ unsigned m_iters_with_no_cost_growing = 0;
|
||||
+ unsigned m_num_factorizations = 0;
|
||||
+ unsigned m_num_of_implied_bounds = 0;
|
||||
+ unsigned m_need_to_solve_inf = 0;
|
||||
+ unsigned m_max_cols = 0;
|
||||
+ unsigned m_max_rows = 0;
|
||||
+ unsigned m_gcd_calls = 0;
|
||||
+ unsigned m_gcd_conflicts = 0;
|
||||
+ unsigned m_cube_calls = 0;
|
||||
+ unsigned m_cube_success = 0;
|
||||
+ unsigned m_patches = 0;
|
||||
+ unsigned m_patches_success = 0;
|
||||
+ unsigned m_hnf_cutter_calls = 0;
|
||||
+ unsigned m_hnf_cuts = 0;
|
||||
+ unsigned m_nla_calls = 0;
|
||||
+ unsigned m_gomory_cuts = 0;
|
||||
+ unsigned m_nla_add_bounds = 0;
|
||||
+ unsigned m_nla_propagate_bounds = 0;
|
||||
+ unsigned m_nla_propagate_eq = 0;
|
||||
+ unsigned m_nla_lemmas = 0;
|
||||
+ unsigned m_nra_calls = 0;
|
||||
+ unsigned m_nla_bounds_improvements = 0;
|
||||
+ unsigned m_horner_calls = 0;
|
||||
+ unsigned m_horner_conflicts = 0;
|
||||
+ unsigned m_cross_nested_forms = 0;
|
||||
+ unsigned m_grobner_calls = 0;
|
||||
+ unsigned m_grobner_conflicts = 0;
|
||||
+ unsigned m_offset_eqs = 0;
|
||||
+ unsigned m_fixed_eqs = 0;
|
||||
statistics() { reset(); }
|
||||
- void reset() { memset(this, 0, sizeof(*this)); }
|
||||
+ void reset() { *this = statistics{}; }
|
||||
void collect_statistics(::statistics& st) const {
|
||||
st.update("arith-factorizations", m_num_factorizations);
|
||||
st.update("arith-make-feasible", m_make_feasible);
|
||||
diff --git src/math/lp/static_matrix.h src/math/lp/static_matrix.h
|
||||
index 9d6bb859964..42dd476b5d4 100644
|
||||
--- src/math/lp/static_matrix.h
|
||||
+++ src/math/lp/static_matrix.h
|
||||
@@ -79,7 +79,7 @@ class static_matrix (public)
|
||||
ref(static_matrix & m, unsigned row, unsigned col):m_matrix(m), m_row(row), m_col(col) {}
|
||||
ref & operator=(T const & v) { m_matrix.set( m_row, m_col, v); return *this; }
|
||||
|
||||
- ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get(v.m_row, v.m_col)); return *this; }
|
||||
+ ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get_elem(v.m_row, v.m_col)); return *this; }
|
||||
|
||||
operator T () const { return m_matrix.get_elem(m_row, m_col); }
|
||||
};
|
||||
diff --git src/math/lp/static_matrix_def.h src/math/lp/static_matrix_def.h
|
||||
index 0370ee8990a..c3b2fc16821 100644
|
||||
--- src/math/lp/static_matrix_def.h
|
||||
+++ src/math/lp/static_matrix_def.h
|
||||
--- src/math/lp/static_matrix_def.h.orig 2024-03-07 18:25:16 UTC
|
||||
+++ src/math/lp/static_matrix_def.h
|
||||
@@ -92,7 +92,7 @@ static_matrix<T, X>::static_matrix(static_matrix const
|
||||
init_row_columns(m, m);
|
||||
for (; m-- > 0; )
|
||||
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));
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::clear() {
|
||||
Loading…
Add table
Reference in a new issue