Skip to content

Commit 2ce89e5

Browse files
authored
Gcc 15 two phase (Z3Prover#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
1 parent 25e683e commit 2ce89e5

File tree

3 files changed

+36
-37
lines changed

3 files changed

+36
-37
lines changed

Diff for: src/math/lp/lp_settings.h

+34-35
Original file line numberDiff line numberDiff line change
@@ -97,42 +97,41 @@ class lp_resource_limit {
9797
};
9898

9999
struct statistics {
100-
unsigned m_make_feasible;
101-
unsigned m_total_iterations;
102-
unsigned m_iters_with_no_cost_growing;
103-
unsigned m_num_factorizations;
104-
unsigned m_num_of_implied_bounds;
105-
unsigned m_need_to_solve_inf;
106-
unsigned m_max_cols;
107-
unsigned m_max_rows;
108-
unsigned m_gcd_calls;
109-
unsigned m_gcd_conflicts;
110-
unsigned m_cube_calls;
111-
unsigned m_cube_success;
112-
unsigned m_patches;
113-
unsigned m_patches_success;
114-
unsigned m_hnf_cutter_calls;
115-
unsigned m_hnf_cuts;
116-
unsigned m_nla_calls;
117-
unsigned m_gomory_cuts;
118-
unsigned m_nla_add_bounds;
119-
unsigned m_nla_propagate_bounds;
120-
unsigned m_nla_propagate_eq;
121-
unsigned m_nla_lemmas;
122-
unsigned m_nra_calls;
123-
unsigned m_nla_bounds_improvements;
124-
unsigned m_horner_calls;
125-
unsigned m_horner_conflicts;
126-
unsigned m_cross_nested_forms;
127-
unsigned m_grobner_calls;
128-
unsigned m_grobner_conflicts;
129-
unsigned m_offset_eqs;
130-
unsigned m_fixed_eqs;
131-
::statistics m_st;
132-
statistics() { reset(); }
100+
unsigned m_make_feasible = 0;
101+
unsigned m_total_iterations = 0;
102+
unsigned m_iters_with_no_cost_growing = 0;
103+
unsigned m_num_factorizations = 0;
104+
unsigned m_num_of_implied_bounds = 0;
105+
unsigned m_need_to_solve_inf = 0;
106+
unsigned m_max_cols = 0;
107+
unsigned m_max_rows = 0;
108+
unsigned m_gcd_calls = 0;
109+
unsigned m_gcd_conflicts = 0;
110+
unsigned m_cube_calls = 0;
111+
unsigned m_cube_success = 0;
112+
unsigned m_patches = 0;
113+
unsigned m_patches_success = 0;
114+
unsigned m_hnf_cutter_calls = 0;
115+
unsigned m_hnf_cuts = 0;
116+
unsigned m_nla_calls = 0;
117+
unsigned m_gomory_cuts = 0;
118+
unsigned m_nla_add_bounds = 0;
119+
unsigned m_nla_propagate_bounds = 0;
120+
unsigned m_nla_propagate_eq = 0;
121+
unsigned m_nla_lemmas = 0;
122+
unsigned m_nra_calls = 0;
123+
unsigned m_nla_bounds_improvements = 0;
124+
unsigned m_horner_calls = 0;
125+
unsigned m_horner_conflicts = 0;
126+
unsigned m_cross_nested_forms = 0;
127+
unsigned m_grobner_calls = 0;
128+
unsigned m_grobner_conflicts = 0;
129+
unsigned m_offset_eqs = 0;
130+
unsigned m_fixed_eqs = 0;
131+
::statistics m_st = {};
132+
133133
void reset() {
134-
memset(this, 0, sizeof(*this));
135-
m_st.reset();
134+
*this = statistics{};
136135
}
137136
void collect_statistics(::statistics& st) const {
138137
st.update("arith-factorizations", m_num_factorizations);

Diff for: src/math/lp/static_matrix.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ class static_matrix
7979
ref(static_matrix & m, unsigned row, unsigned col):m_matrix(m), m_row(row), m_col(col) {}
8080
ref & operator=(T const & v) { m_matrix.set( m_row, m_col, v); return *this; }
8181

82-
ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get(v.m_row, v.m_col)); return *this; }
82+
ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get_elem(v.m_row, v.m_col)); return *this; }
8383

8484
operator T () const { return m_matrix.get_elem(m_row, m_col); }
8585
};

Diff for: src/math/lp/static_matrix_def.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
9292
init_row_columns(m, m);
9393
for (; m-- > 0; )
9494
for (auto & col : A.m_columns[m])
95-
set(col.var(), m, A.get_value_of_column_cell(col));
95+
set(col.var(), m, A.get_column_cell(col));
9696
}
9797

9898
template <typename T, typename X> void static_matrix<T, X>::clear() {

0 commit comments

Comments
 (0)