From 7e3aad4e177972ab8969b025dd59fa407dbfd9e0 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Mon, 8 Jun 2026 10:19:18 -0700 Subject: [PATCH 01/13] Fixes necessary to compile z3 included in clang-tidy via FetchContents. --- src/api/CMakeLists.txt | 2 +- src/api/c++/z3++.h | 6 +++--- src/opt/CMakeLists.txt | 2 +- src/shell/CMakeLists.txt | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index c1e78f473..c6ad57c70 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -66,7 +66,7 @@ z3_add_component(api z3_replayer.cpp ${full_path_generated_files} COMPONENT_DEPENDENCIES - opt + z3_opt euf portfolio realclosure diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f66bd1f76..9e8cc6796 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4925,7 +4925,7 @@ namespace z3 { void check_context(rcf_num const& other) const { if (m_ctx != other.m_ctx) { - throw exception("rcf_num objects from different contexts"); + Z3_THROW(exception("rcf_num objects from different contexts")); } } @@ -5105,9 +5105,9 @@ namespace z3 { */ inline std::vector rcf_roots(context& c, std::vector const& coeffs) { if (coeffs.empty()) { - throw exception("polynomial coefficients cannot be empty"); + Z3_THROW(exception("polynomial coefficients cannot be empty")); } - + unsigned n = static_cast(coeffs.size()); std::vector a(n); std::vector roots(n); diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index 21075d88c..85b716306 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -1,4 +1,4 @@ -z3_add_component(opt +z3_add_component(z3_opt SOURCES maxcore.cpp maxlex.cpp diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c0e9c8505..22c071966 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -8,7 +8,7 @@ set (shell_object_files "") # We are only using these dependencies to enforce a build # order. We don't use this list for actual linking. -set(shell_deps api extra_cmds opt sat) +set(shell_deps api extra_cmds z3_opt sat) z3_expand_dependencies(shell_expanded_deps ${shell_deps}) get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS) foreach (component ${Z3_LIBZ3_COMPONENTS_LIST}) From fe2b6fac24acd968ccf27f5e1e0603a819b9cea2 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Mon, 8 Jun 2026 11:25:43 -0700 Subject: [PATCH 02/13] Introduce (and use) a macro for the "trailing array" idiom, so we can disable warnings for this when they're in force. --- cmake/compiler_warnings.cmake | 1 + src/ast/ast.h | 7 ++++--- src/ast/euf/euf_enode.h | 3 ++- src/ast/euf/euf_mam.cpp | 9 +++++---- src/ast/rewriter/cached_var_subst.h | 3 ++- src/ast/simplifiers/euf_completion.h | 3 ++- src/math/polynomial/polynomial.cpp | 3 ++- src/math/polynomial/rpolynomial.cpp | 3 ++- src/math/subpaving/subpaving_t.h | 5 +++-- src/muz/base/dl_rule.h | 3 ++- src/nlsat/nlsat_clause.h | 3 ++- src/nlsat/nlsat_interval_set.cpp | 3 ++- src/nlsat/nlsat_justification.h | 3 ++- src/nlsat/nlsat_types.h | 3 ++- src/sat/sat_clause.h | 3 ++- src/sat/sat_lookahead.h | 3 ++- src/sat/smt/ba_xor.h | 3 ++- src/sat/smt/pb_card.h | 3 ++- src/sat/smt/pb_pb.h | 3 ++- src/sat/smt/q_clause.h | 3 ++- src/sat/smt/q_solver.h | 3 ++- src/sat/smt/sat_smt.h | 3 ++- src/smt/mam.cpp | 9 +++++---- src/smt/smt_clause.h | 3 ++- src/smt/smt_enode.h | 3 ++- src/smt/smt_quantifier_instances.h | 3 ++- src/util/mpz.h | 3 ++- src/util/sexpr.cpp | 3 ++- src/util/trailing_array.h | 29 ++++++++++++++++++++++++++++ 29 files changed, 93 insertions(+), 36 deletions(-) create mode 100644 src/util/trailing_array.h diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index ddd96c047..0f9e9d09a 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -12,6 +12,7 @@ set(GCC_ONLY_WARNINGS "") set(CLANG_ONLY_WARNINGS "-Wno-c++98-compat" "-Wno-c++98-compat-pedantic" + "-Wzero-length-array" ) set(MSVC_WARNINGS "/W3") diff --git a/src/ast/ast.h b/src/ast/ast.h index 03713ee4b..0922ad759 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -20,6 +20,7 @@ Revision History: #include "util/vector.h" +#include "util/trailing_array.h" #include "util/hashtable.h" #include "util/buffer.h" #include "util/zstring.h" @@ -642,7 +643,7 @@ class func_decl : public decl { unsigned m_arity; sort * m_range; - sort * m_domain[0]; + TRAILING_ARRAY(sort *, m_domain); static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); } @@ -725,7 +726,7 @@ class app : public expr { func_decl * m_decl; unsigned m_num_args; app_flags m_flags; - expr * m_args[0]; + TRAILING_ARRAY(expr *, m_args); static unsigned get_obj_size(unsigned num_args) { return sizeof(app) + num_args * sizeof(expr *); @@ -872,7 +873,7 @@ class quantifier : public expr { symbol m_skid; unsigned m_num_patterns; unsigned m_num_no_patterns; - char m_patterns_decls[0]; + TRAILING_ARRAY(char, m_patterns_decls); static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*)); diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index af22a5b2c..b6bd5302a 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -16,6 +16,7 @@ Author: --*/ #include "util/vector.h" +#include "util/trailing_array.h" #include "util/id_var_list.h" #include "util/lbool.h" #include "util/approx_set.h" @@ -66,7 +67,7 @@ namespace euf { signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; - enode* m_args[0]; + TRAILING_ARRAY(enode*, m_args); friend class enode_args; friend class enode_parents; diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index 8148fe7d9..686b0d938 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -20,6 +20,7 @@ Revision History: --*/ #include +#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -231,7 +232,7 @@ namespace euf { The size of the array is m_num_args. */ - enode * m_joints[0]; + TRAILING_ARRAY(enode *, m_joints); }; struct bind : public instruction { @@ -247,21 +248,21 @@ namespace euf { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - unsigned m_iregs[0]; + TRAILING_ARRAY(unsigned, m_iregs); }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - unsigned m_bindings[0]; + TRAILING_ARRAY(unsigned, m_bindings); }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - unsigned m_iregs[0]; + TRAILING_ARRAY(unsigned, m_iregs); }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/ast/rewriter/cached_var_subst.h b/src/ast/rewriter/cached_var_subst.h index ad9364967..530f57404 100644 --- a/src/ast/rewriter/cached_var_subst.h +++ b/src/ast/rewriter/cached_var_subst.h @@ -19,13 +19,14 @@ Revision History: #pragma once #include "ast/rewriter/var_subst.h" +#include "util/trailing_array.h" #include "util/map.h" class cached_var_subst { struct key { quantifier * m_qa; unsigned m_num_bindings; - expr * m_bindings[0]; + TRAILING_ARRAY(expr *, m_bindings); }; struct key_hash_proc { unsigned operator()(key * k) const { diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index 97fc45a42..7076734ba 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -21,6 +21,7 @@ Author: #pragma once #include "util/scoped_vector.h" +#include "util/trailing_array.h" #include "util/dlist.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/euf/euf_egraph.h" @@ -53,7 +54,7 @@ namespace euf { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - euf::enode* m_nodes[0]; + TRAILING_ARRAY(euf::enode*, m_nodes); binding(quantifier* q, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) : m_q(q), diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 1b06fb2b0..b846d7da3 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "math/polynomial/polynomial.h" +#include "util/trailing_array.h" #include "util/vector.h" #include "util/chashtable.h" #include "util/small_object_allocator.h" @@ -160,7 +161,7 @@ namespace polynomial { unsigned m_total_degree; //!< total degree of the monomial unsigned m_size; //!< number of powers unsigned m_hash; - power m_powers[0]; + TRAILING_ARRAY(power, m_powers); friend class tmp_monomial; void sort() { diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp index 67b882525..181aaf64e 100644 --- a/src/math/polynomial/rpolynomial.cpp +++ b/src/math/polynomial/rpolynomial.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "math/polynomial/rpolynomial.h" +#include "util/trailing_array.h" #include "util/tptr.h" #include "util/buffer.h" @@ -39,7 +40,7 @@ namespace rpolynomial { unsigned m_ref_count; var m_var; unsigned m_size; - poly_or_num * m_args[0]; + TRAILING_ARRAY(poly_or_num *, m_args); public: unsigned ref_count() const { return m_ref_count; } diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 7300e3da3..3cf14da67 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include +#include "util/trailing_array.h" #include "util/tptr.h" #include "util/small_object_allocator.h" #include "util/chashtable.h" @@ -94,7 +95,7 @@ public: unsigned m_lemma:1; //!< True if it is a learned clause. unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched. unsigned m_num_jst:30; //!< Number of times it is used to justify some bound. - ineq * m_atoms[0]; + TRAILING_ARRAY(ineq *, m_atoms); static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); } public: clause():constraint(constraint::CLAUSE) {} @@ -322,7 +323,7 @@ public: class monomial : public definition { friend class context_t; unsigned m_size; - power m_powers[0]; + TRAILING_ARRAY(power, m_powers); monomial(unsigned sz, power const * pws); static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); } public: diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 87c2637a9..1b304454d 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -20,6 +20,7 @@ Revision History: #pragma once #include "ast/ast.h" +#include "util/trailing_array.h" #include "muz/base/dl_costs.h" #include "muz/base/dl_util.h" #include "ast/used_vars.h" @@ -308,7 +309,7 @@ namespace datalog { The negated flag is never set for interpreted tails. */ - app * m_tail[0]; + TRAILING_ARRAY(app *, m_tail); static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h index 91467303c..667f39bae 100644 --- a/src/nlsat/nlsat_clause.h +++ b/src/nlsat/nlsat_clause.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" +#include "util/trailing_array.h" #include "util/vector.h" namespace nlsat { @@ -34,7 +35,7 @@ namespace nlsat { unsigned m_marked:1; unsigned m_var_hash; assumption_set m_assumptions; - literal m_lits[0]; + TRAILING_ARRAY(literal, m_lits); static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } clause(unsigned id, unsigned sz, literal const * lits, bool learned, assumption_set as); diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index dc5740e10..9f8a8d7cc 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "nlsat/nlsat_interval_set.h" +#include "util/trailing_array.h" #include "math/polynomial/algebraic_numbers.h" #include "util/buffer.h" @@ -39,7 +40,7 @@ namespace nlsat { unsigned m_num_intervals; unsigned m_ref_count:31; unsigned m_full:1; - interval m_intervals[0]; + TRAILING_ARRAY(interval, m_intervals); }; void display(std::ostream & out, anum_manager & am, interval const & curr) { diff --git a/src/nlsat/nlsat_justification.h b/src/nlsat/nlsat_justification.h index d9567ebf9..9b1344298 100644 --- a/src/nlsat/nlsat_justification.h +++ b/src/nlsat/nlsat_justification.h @@ -20,6 +20,7 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" +#include "util/trailing_array.h" #include "util/tptr.h" namespace nlsat { @@ -38,7 +39,7 @@ namespace nlsat { class lazy_justification { unsigned m_num_literals; unsigned m_num_clauses; - char m_data[0]; + TRAILING_ARRAY(char, m_data); nlsat::clause* const* clauses() const { return (nlsat::clause *const*)(m_data); } public: static unsigned get_obj_size(unsigned nl, unsigned nc) { return sizeof(lazy_justification) + sizeof(literal)*nl + sizeof(nlsat::clause*)*nc; } diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index be8f625c9..b79cb428c 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "math/polynomial/polynomial.h" +#include "util/trailing_array.h" #include "util/buffer.h" #include "sat/sat_types.h" #include "util/z3_exception.h" @@ -99,7 +100,7 @@ namespace nlsat { class ineq_atom : public atom { friend class solver; unsigned m_size; - poly * m_ps[0]; + TRAILING_ARRAY(poly *, m_ps); ineq_atom(kind k, unsigned sz, poly * const * ps, bool const * is_even, var max_var); static unsigned get_obj_size(unsigned sz) { return sizeof(ineq_atom) + sizeof(poly*)*sz; } public: diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 0129febbf..1635def8e 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "util/small_object_allocator.h" +#include "util/trailing_array.h" #include "util/id_gen.h" #include "util/map.h" #include "sat/sat_types.h" @@ -53,7 +54,7 @@ namespace sat { unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc - literal m_lits[0]; + TRAILING_ARRAY(literal, m_lits); static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 87757ba59..954a09fb4 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -21,6 +21,7 @@ Notes: #include "util/small_object_allocator.h" +#include "util/trailing_array.h" #include "sat/sat_elim_eqs.h" namespace pb { @@ -147,7 +148,7 @@ namespace sat { unsigned m_size; // number of non-false literals size_t m_obj_size; // object size (counting all literals) literal m_head; // head literal - literal m_literals[0]; // list of literals, put any true literal in head. + TRAILING_ARRAY(literal, m_literals); // list of literals, put any true literal in head. size_t num_lits() const { return (m_obj_size - sizeof(nary)) / sizeof(literal); } diff --git a/src/sat/smt/ba_xor.h b/src/sat/smt/ba_xor.h index 009534951..b61e47c04 100644 --- a/src/sat/smt/ba_xor.h +++ b/src/sat/smt/ba_xor.h @@ -18,13 +18,14 @@ Author: #pragma once #include "sat/sat_types.h" +#include "util/trailing_array.h" #include "sat/smt/ba_constraint.h" namespace ba { class xr : public constraint { - literal m_lits[0]; + TRAILING_ARRAY(literal, m_lits); public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(xr) + num_lits * sizeof(literal)); } xr(unsigned id, literal_vector const& lits); diff --git a/src/sat/smt/pb_card.h b/src/sat/smt/pb_card.h index 26c6d3bb1..184b8259a 100644 --- a/src/sat/smt/pb_card.h +++ b/src/sat/smt/pb_card.h @@ -18,13 +18,14 @@ Author: #pragma once #include "sat/sat_types.h" +#include "util/trailing_array.h" #include "sat/smt/pb_constraint.h" namespace pb { class card : public constraint { - literal m_lits[0]; + TRAILING_ARRAY(literal, m_lits); public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(card) + num_lits * sizeof(literal)); } card(unsigned id, literal lit, literal_vector const& lits, unsigned k); diff --git a/src/sat/smt/pb_pb.h b/src/sat/smt/pb_pb.h index 5386051af..7e020afaa 100644 --- a/src/sat/smt/pb_pb.h +++ b/src/sat/smt/pb_pb.h @@ -18,6 +18,7 @@ Author: #pragma once #include "sat/sat_types.h" +#include "util/trailing_array.h" #include "sat/smt/pb_card.h" @@ -27,7 +28,7 @@ namespace pb { unsigned m_slack; unsigned m_num_watch; unsigned m_max_sum; - wliteral m_wlits[0]; + TRAILING_ARRAY(wliteral, m_wlits); public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(pbc) + num_lits * sizeof(wliteral)); } pbc(unsigned id, literal lit, svector const& wlits, unsigned k); diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index aedb0bc4c..0fb3636cb 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -17,6 +17,7 @@ Author: #pragma once #include "util/dlist.h" +#include "util/trailing_array.h" #include "ast/ast.h" #include "ast/quantifier_stat.h" #include "ast/euf/euf_enode.h" @@ -66,7 +67,7 @@ namespace q { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - euf::enode* m_nodes[0]; + TRAILING_ARRAY(euf::enode*, m_nodes); binding(clause& c, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top): c(&c), diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index a7220e68b..40b8195a7 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -17,6 +17,7 @@ Author: #pragma once #include "util/obj_hashtable.h" +#include "util/trailing_array.h" #include "ast/ast_trail.h" #include "ast/rewriter/der.h" #include "sat/smt/sat_th.h" @@ -35,7 +36,7 @@ namespace q { unsigned m_num_bindings; unsigned m_num_literals; sat::literal* m_literals; - expr* m_bindings[0]; + TRAILING_ARRAY(expr*, m_bindings); q_proof_hint(symbol const& method, unsigned g, unsigned b, unsigned l) { m_method = method; diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index c661288f5..51134d6df 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -16,6 +16,7 @@ Author: --*/ #pragma once #include "ast/ast.h" +#include "util/trailing_array.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/sat_solver.h" @@ -31,7 +32,7 @@ namespace sat { class constraint_base { extension* m_ex = nullptr; - unsigned m_mem[0]; + TRAILING_ARRAY(unsigned, m_mem); static size_t ext_size() { return sizeof(((constraint_base*)nullptr)->m_ex); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 80918fcb4..aa04851a4 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -207,7 +208,7 @@ namespace { The size of the array is m_num_args. */ - enode * m_joints[0]; + TRAILING_ARRAY(enode *, m_joints); }; struct bind : public instruction { @@ -223,21 +224,21 @@ namespace { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - unsigned m_iregs[0]; + TRAILING_ARRAY(unsigned, m_iregs); }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - unsigned m_bindings[0]; + TRAILING_ARRAY(unsigned, m_bindings); }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - unsigned m_iregs[0]; + TRAILING_ARRAY(unsigned, m_iregs); }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index 89d8f2d66..c1f50edcb 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "ast/ast.h" +#include "util/trailing_array.h" #include "smt/smt_literal.h" #include "util/tptr.h" #include "util/obj_hashtable.h" @@ -62,7 +63,7 @@ namespace smt { unsigned m_has_del_eh:1; //!< true if must notify event handler when deleted. unsigned m_has_justification:1; //!< true if the clause has a justification attached to it. unsigned m_deleted:1; //!< true if the clause is marked for deletion by was not deleted yet because it is referenced by some data-structure (e.g., m_lemmas) - literal m_lits[0]; + TRAILING_ARRAY(literal, m_lits); static unsigned get_obj_size(unsigned num_lits, clause_kind k, bool has_atoms, bool has_del_eh, bool has_justification) { unsigned r = sizeof(clause) + sizeof(literal) * num_lits; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index e9dc4c4e1..84ffe9def 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "util/id_var_list.h" +#include "util/trailing_array.h" #include "util/approx_set.h" #include "ast/ast.h" #include "ast/ast_pp.h" @@ -101,7 +102,7 @@ namespace smt { trans_justification m_trans; //!< A justification for the enode being equal to its root. approx_set m_lbls; approx_set m_plbls; - enode * m_args[0]; //!< Cached args + TRAILING_ARRAY(enode *, m_args); //!< Cached args friend class context; friend class conflict_resolution; diff --git a/src/smt/smt_quantifier_instances.h b/src/smt/smt_quantifier_instances.h index 6bd76a335..d8b95f807 100644 --- a/src/smt/smt_quantifier_instances.h +++ b/src/smt/smt_quantifier_instances.h @@ -1,3 +1,4 @@ +#include "util/trailing_array.h" /*++ Copyright (c) 2006 Microsoft Corporation @@ -25,7 +26,7 @@ namespace smt { class quantifier_instance { quantifier * m_quantifier; double m_cost; - enode * m_enodes[0]; + TRAILING_ARRAY(enode *, m_enodes); quantifier_instance(quantifier * q, enode * const * enodes); friend class quantifier_instances; public: diff --git a/src/util/mpz.h b/src/util/mpz.h index 7b714b9be..7aa85ed24 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include +#include "util/trailing_array.h" #include "util/mutex.h" #include "util/util.h" #include "util/small_object_allocator.h" @@ -57,7 +58,7 @@ typedef unsigned int digit_t; class mpz_cell { unsigned m_size; unsigned m_capacity; - digit_t m_digits[0]; + TRAILING_ARRAY(digit_t, m_digits); friend class mpz_manager; friend class mpz_manager; friend class mpz_stack; diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 4b0b8378d..bc2cd3295 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "util/sexpr.h" +#include "util/trailing_array.h" #include "util/vector.h" #include "util/buffer.h" @@ -27,7 +28,7 @@ Notes: struct sexpr_composite : public sexpr { unsigned m_num_children; - sexpr * m_children[0]; + TRAILING_ARRAY(sexpr *, m_children); sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos): sexpr(kind_t::COMPOSITE, line, pos), m_num_children(num_children) { diff --git a/src/util/trailing_array.h b/src/util/trailing_array.h new file mode 100644 index 000000000..aecfec974 --- /dev/null +++ b/src/util/trailing_array.h @@ -0,0 +1,29 @@ +#pragma once + +// Copyright (c) Microsoft Corporation. All Rights Reserved. + +// Many classes in Z3 use the "trailing array" idiom: the last field +// of the class C is a zero-length array of some type T, and the allocation +// of an instance adds extra space for some number of T's (usually the +// number is held in some other field of C). + +// Zero-length arrays are non-standard, and provoke a warning in Clang +// when -Wzero-length-array is specified. This file introduces a macro +// for this idiom, which, for compilers that give a warning, disables +// the warning around the declaration. So far that's only Clang, +// but more could be added. + +#define STR_PRAGMA_FOR_TRAILING_ARRAY(x) _Pragma(#x) + +#ifdef __clang__ +#define TRAILING_ARRAY(type, field) \ + STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic push) \ + STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic ignored "-Wzero-length-array") \ + type field[0]; \ + STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic pop) + +#else +#define TRAILING_ARRAY(type, field) type field[0]; + +#endif + From 2afc3db49c2fdc7881087e7239914b5e31cab670 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 11 Jun 2026 13:15:08 -0700 Subject: [PATCH 03/13] Undo previous changes; use a much simpler solution. --- src/ast/ast.h | 7 +++---- src/ast/euf/euf_enode.h | 3 +-- src/ast/euf/euf_mam.cpp | 9 ++++----- src/ast/rewriter/cached_var_subst.h | 3 +-- src/ast/simplifiers/euf_completion.h | 3 +-- src/math/polynomial/polynomial.cpp | 3 +-- src/math/polynomial/rpolynomial.cpp | 3 +-- src/math/subpaving/subpaving_t.h | 5 ++--- src/muz/base/dl_rule.h | 3 +-- src/nlsat/nlsat_clause.h | 3 +-- src/nlsat/nlsat_interval_set.cpp | 3 +-- src/nlsat/nlsat_justification.h | 3 +-- src/nlsat/nlsat_types.h | 3 +-- src/sat/sat_clause.h | 3 +-- src/sat/sat_lookahead.h | 3 +-- src/sat/smt/ba_xor.h | 3 +-- src/sat/smt/pb_card.h | 3 +-- src/sat/smt/pb_pb.h | 3 +-- src/sat/smt/q_clause.h | 3 +-- src/sat/smt/q_solver.h | 3 +-- src/sat/smt/sat_smt.h | 3 +-- src/smt/mam.cpp | 9 ++++----- src/smt/smt_clause.h | 3 +-- src/smt/smt_enode.h | 3 +-- src/smt/smt_quantifier_instances.h | 3 +-- src/util/mpz.h | 3 +-- src/util/sexpr.cpp | 3 +-- src/util/trailing_array.h | 29 ---------------------------- 28 files changed, 36 insertions(+), 92 deletions(-) delete mode 100644 src/util/trailing_array.h diff --git a/src/ast/ast.h b/src/ast/ast.h index 0922ad759..03713ee4b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -20,7 +20,6 @@ Revision History: #include "util/vector.h" -#include "util/trailing_array.h" #include "util/hashtable.h" #include "util/buffer.h" #include "util/zstring.h" @@ -643,7 +642,7 @@ class func_decl : public decl { unsigned m_arity; sort * m_range; - TRAILING_ARRAY(sort *, m_domain); + sort * m_domain[0]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); } @@ -726,7 +725,7 @@ class app : public expr { func_decl * m_decl; unsigned m_num_args; app_flags m_flags; - TRAILING_ARRAY(expr *, m_args); + expr * m_args[0]; static unsigned get_obj_size(unsigned num_args) { return sizeof(app) + num_args * sizeof(expr *); @@ -873,7 +872,7 @@ class quantifier : public expr { symbol m_skid; unsigned m_num_patterns; unsigned m_num_no_patterns; - TRAILING_ARRAY(char, m_patterns_decls); + char m_patterns_decls[0]; static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*)); diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index b6bd5302a..af22a5b2c 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -16,7 +16,6 @@ Author: --*/ #include "util/vector.h" -#include "util/trailing_array.h" #include "util/id_var_list.h" #include "util/lbool.h" #include "util/approx_set.h" @@ -67,7 +66,7 @@ namespace euf { signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; - TRAILING_ARRAY(enode*, m_args); + enode* m_args[0]; friend class enode_args; friend class enode_parents; diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index 686b0d938..8148fe7d9 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -20,7 +20,6 @@ Revision History: --*/ #include -#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -232,7 +231,7 @@ namespace euf { The size of the array is m_num_args. */ - TRAILING_ARRAY(enode *, m_joints); + enode * m_joints[0]; }; struct bind : public instruction { @@ -248,21 +247,21 @@ namespace euf { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - TRAILING_ARRAY(unsigned, m_bindings); + unsigned m_bindings[0]; }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/ast/rewriter/cached_var_subst.h b/src/ast/rewriter/cached_var_subst.h index 530f57404..ad9364967 100644 --- a/src/ast/rewriter/cached_var_subst.h +++ b/src/ast/rewriter/cached_var_subst.h @@ -19,14 +19,13 @@ Revision History: #pragma once #include "ast/rewriter/var_subst.h" -#include "util/trailing_array.h" #include "util/map.h" class cached_var_subst { struct key { quantifier * m_qa; unsigned m_num_bindings; - TRAILING_ARRAY(expr *, m_bindings); + expr * m_bindings[0]; }; struct key_hash_proc { unsigned operator()(key * k) const { diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index 7076734ba..97fc45a42 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -21,7 +21,6 @@ Author: #pragma once #include "util/scoped_vector.h" -#include "util/trailing_array.h" #include "util/dlist.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/euf/euf_egraph.h" @@ -54,7 +53,7 @@ namespace euf { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - TRAILING_ARRAY(euf::enode*, m_nodes); + euf::enode* m_nodes[0]; binding(quantifier* q, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) : m_q(q), diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index b846d7da3..1b06fb2b0 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "math/polynomial/polynomial.h" -#include "util/trailing_array.h" #include "util/vector.h" #include "util/chashtable.h" #include "util/small_object_allocator.h" @@ -161,7 +160,7 @@ namespace polynomial { unsigned m_total_degree; //!< total degree of the monomial unsigned m_size; //!< number of powers unsigned m_hash; - TRAILING_ARRAY(power, m_powers); + power m_powers[0]; friend class tmp_monomial; void sort() { diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp index 181aaf64e..67b882525 100644 --- a/src/math/polynomial/rpolynomial.cpp +++ b/src/math/polynomial/rpolynomial.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "math/polynomial/rpolynomial.h" -#include "util/trailing_array.h" #include "util/tptr.h" #include "util/buffer.h" @@ -40,7 +39,7 @@ namespace rpolynomial { unsigned m_ref_count; var m_var; unsigned m_size; - TRAILING_ARRAY(poly_or_num *, m_args); + poly_or_num * m_args[0]; public: unsigned ref_count() const { return m_ref_count; } diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 3cf14da67..7300e3da3 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include -#include "util/trailing_array.h" #include "util/tptr.h" #include "util/small_object_allocator.h" #include "util/chashtable.h" @@ -95,7 +94,7 @@ public: unsigned m_lemma:1; //!< True if it is a learned clause. unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched. unsigned m_num_jst:30; //!< Number of times it is used to justify some bound. - TRAILING_ARRAY(ineq *, m_atoms); + ineq * m_atoms[0]; static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); } public: clause():constraint(constraint::CLAUSE) {} @@ -323,7 +322,7 @@ public: class monomial : public definition { friend class context_t; unsigned m_size; - TRAILING_ARRAY(power, m_powers); + power m_powers[0]; monomial(unsigned sz, power const * pws); static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); } public: diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 1b304454d..87c2637a9 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -20,7 +20,6 @@ Revision History: #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "muz/base/dl_costs.h" #include "muz/base/dl_util.h" #include "ast/used_vars.h" @@ -309,7 +308,7 @@ namespace datalog { The negated flag is never set for interpreted tails. */ - TRAILING_ARRAY(app *, m_tail); + app * m_tail[0]; static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h index 667f39bae..91467303c 100644 --- a/src/nlsat/nlsat_clause.h +++ b/src/nlsat/nlsat_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" -#include "util/trailing_array.h" #include "util/vector.h" namespace nlsat { @@ -35,7 +34,7 @@ namespace nlsat { unsigned m_marked:1; unsigned m_var_hash; assumption_set m_assumptions; - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } clause(unsigned id, unsigned sz, literal const * lits, bool learned, assumption_set as); diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 9f8a8d7cc..dc5740e10 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include "nlsat/nlsat_interval_set.h" -#include "util/trailing_array.h" #include "math/polynomial/algebraic_numbers.h" #include "util/buffer.h" @@ -40,7 +39,7 @@ namespace nlsat { unsigned m_num_intervals; unsigned m_ref_count:31; unsigned m_full:1; - TRAILING_ARRAY(interval, m_intervals); + interval m_intervals[0]; }; void display(std::ostream & out, anum_manager & am, interval const & curr) { diff --git a/src/nlsat/nlsat_justification.h b/src/nlsat/nlsat_justification.h index 9b1344298..d9567ebf9 100644 --- a/src/nlsat/nlsat_justification.h +++ b/src/nlsat/nlsat_justification.h @@ -20,7 +20,6 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" -#include "util/trailing_array.h" #include "util/tptr.h" namespace nlsat { @@ -39,7 +38,7 @@ namespace nlsat { class lazy_justification { unsigned m_num_literals; unsigned m_num_clauses; - TRAILING_ARRAY(char, m_data); + char m_data[0]; nlsat::clause* const* clauses() const { return (nlsat::clause *const*)(m_data); } public: static unsigned get_obj_size(unsigned nl, unsigned nc) { return sizeof(lazy_justification) + sizeof(literal)*nl + sizeof(nlsat::clause*)*nc; } diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index b79cb428c..be8f625c9 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "math/polynomial/polynomial.h" -#include "util/trailing_array.h" #include "util/buffer.h" #include "sat/sat_types.h" #include "util/z3_exception.h" @@ -100,7 +99,7 @@ namespace nlsat { class ineq_atom : public atom { friend class solver; unsigned m_size; - TRAILING_ARRAY(poly *, m_ps); + poly * m_ps[0]; ineq_atom(kind k, unsigned sz, poly * const * ps, bool const * is_even, var max_var); static unsigned get_obj_size(unsigned sz) { return sizeof(ineq_atom) + sizeof(poly*)*sz; } public: diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1635def8e..0129febbf 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "util/small_object_allocator.h" -#include "util/trailing_array.h" #include "util/id_gen.h" #include "util/map.h" #include "sat/sat_types.h" @@ -54,7 +53,7 @@ namespace sat { unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 954a09fb4..87757ba59 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -21,7 +21,6 @@ Notes: #include "util/small_object_allocator.h" -#include "util/trailing_array.h" #include "sat/sat_elim_eqs.h" namespace pb { @@ -148,7 +147,7 @@ namespace sat { unsigned m_size; // number of non-false literals size_t m_obj_size; // object size (counting all literals) literal m_head; // head literal - TRAILING_ARRAY(literal, m_literals); // list of literals, put any true literal in head. + literal m_literals[0]; // list of literals, put any true literal in head. size_t num_lits() const { return (m_obj_size - sizeof(nary)) / sizeof(literal); } diff --git a/src/sat/smt/ba_xor.h b/src/sat/smt/ba_xor.h index b61e47c04..009534951 100644 --- a/src/sat/smt/ba_xor.h +++ b/src/sat/smt/ba_xor.h @@ -18,14 +18,13 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/ba_constraint.h" namespace ba { class xr : public constraint { - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(xr) + num_lits * sizeof(literal)); } xr(unsigned id, literal_vector const& lits); diff --git a/src/sat/smt/pb_card.h b/src/sat/smt/pb_card.h index 184b8259a..26c6d3bb1 100644 --- a/src/sat/smt/pb_card.h +++ b/src/sat/smt/pb_card.h @@ -18,14 +18,13 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/pb_constraint.h" namespace pb { class card : public constraint { - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(card) + num_lits * sizeof(literal)); } card(unsigned id, literal lit, literal_vector const& lits, unsigned k); diff --git a/src/sat/smt/pb_pb.h b/src/sat/smt/pb_pb.h index 7e020afaa..5386051af 100644 --- a/src/sat/smt/pb_pb.h +++ b/src/sat/smt/pb_pb.h @@ -18,7 +18,6 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/pb_card.h" @@ -28,7 +27,7 @@ namespace pb { unsigned m_slack; unsigned m_num_watch; unsigned m_max_sum; - TRAILING_ARRAY(wliteral, m_wlits); + wliteral m_wlits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(pbc) + num_lits * sizeof(wliteral)); } pbc(unsigned id, literal lit, svector const& wlits, unsigned k); diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 0fb3636cb..aedb0bc4c 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -17,7 +17,6 @@ Author: #pragma once #include "util/dlist.h" -#include "util/trailing_array.h" #include "ast/ast.h" #include "ast/quantifier_stat.h" #include "ast/euf/euf_enode.h" @@ -67,7 +66,7 @@ namespace q { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - TRAILING_ARRAY(euf::enode*, m_nodes); + euf::enode* m_nodes[0]; binding(clause& c, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top): c(&c), diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 40b8195a7..a7220e68b 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -17,7 +17,6 @@ Author: #pragma once #include "util/obj_hashtable.h" -#include "util/trailing_array.h" #include "ast/ast_trail.h" #include "ast/rewriter/der.h" #include "sat/smt/sat_th.h" @@ -36,7 +35,7 @@ namespace q { unsigned m_num_bindings; unsigned m_num_literals; sat::literal* m_literals; - TRAILING_ARRAY(expr*, m_bindings); + expr* m_bindings[0]; q_proof_hint(symbol const& method, unsigned g, unsigned b, unsigned l) { m_method = method; diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 51134d6df..c661288f5 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -16,7 +16,6 @@ Author: --*/ #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/sat_solver.h" @@ -32,7 +31,7 @@ namespace sat { class constraint_base { extension* m_ex = nullptr; - TRAILING_ARRAY(unsigned, m_mem); + unsigned m_mem[0]; static size_t ext_size() { return sizeof(((constraint_base*)nullptr)->m_ex); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index aa04851a4..80918fcb4 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include -#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -208,7 +207,7 @@ namespace { The size of the array is m_num_args. */ - TRAILING_ARRAY(enode *, m_joints); + enode * m_joints[0]; }; struct bind : public instruction { @@ -224,21 +223,21 @@ namespace { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - TRAILING_ARRAY(unsigned, m_bindings); + unsigned m_bindings[0]; }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index c1f50edcb..89d8f2d66 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "smt/smt_literal.h" #include "util/tptr.h" #include "util/obj_hashtable.h" @@ -63,7 +62,7 @@ namespace smt { unsigned m_has_del_eh:1; //!< true if must notify event handler when deleted. unsigned m_has_justification:1; //!< true if the clause has a justification attached to it. unsigned m_deleted:1; //!< true if the clause is marked for deletion by was not deleted yet because it is referenced by some data-structure (e.g., m_lemmas) - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static unsigned get_obj_size(unsigned num_lits, clause_kind k, bool has_atoms, bool has_del_eh, bool has_justification) { unsigned r = sizeof(clause) + sizeof(literal) * num_lits; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 84ffe9def..e9dc4c4e1 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "util/id_var_list.h" -#include "util/trailing_array.h" #include "util/approx_set.h" #include "ast/ast.h" #include "ast/ast_pp.h" @@ -102,7 +101,7 @@ namespace smt { trans_justification m_trans; //!< A justification for the enode being equal to its root. approx_set m_lbls; approx_set m_plbls; - TRAILING_ARRAY(enode *, m_args); //!< Cached args + enode * m_args[0]; //!< Cached args friend class context; friend class conflict_resolution; diff --git a/src/smt/smt_quantifier_instances.h b/src/smt/smt_quantifier_instances.h index d8b95f807..6bd76a335 100644 --- a/src/smt/smt_quantifier_instances.h +++ b/src/smt/smt_quantifier_instances.h @@ -1,4 +1,3 @@ -#include "util/trailing_array.h" /*++ Copyright (c) 2006 Microsoft Corporation @@ -26,7 +25,7 @@ namespace smt { class quantifier_instance { quantifier * m_quantifier; double m_cost; - TRAILING_ARRAY(enode *, m_enodes); + enode * m_enodes[0]; quantifier_instance(quantifier * q, enode * const * enodes); friend class quantifier_instances; public: diff --git a/src/util/mpz.h b/src/util/mpz.h index 7aa85ed24..7b714b9be 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include -#include "util/trailing_array.h" #include "util/mutex.h" #include "util/util.h" #include "util/small_object_allocator.h" @@ -58,7 +57,7 @@ typedef unsigned int digit_t; class mpz_cell { unsigned m_size; unsigned m_capacity; - TRAILING_ARRAY(digit_t, m_digits); + digit_t m_digits[0]; friend class mpz_manager; friend class mpz_manager; friend class mpz_stack; diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index bc2cd3295..4b0b8378d 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "util/sexpr.h" -#include "util/trailing_array.h" #include "util/vector.h" #include "util/buffer.h" @@ -28,7 +27,7 @@ Notes: struct sexpr_composite : public sexpr { unsigned m_num_children; - TRAILING_ARRAY(sexpr *, m_children); + sexpr * m_children[0]; sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos): sexpr(kind_t::COMPOSITE, line, pos), m_num_children(num_children) { diff --git a/src/util/trailing_array.h b/src/util/trailing_array.h deleted file mode 100644 index aecfec974..000000000 --- a/src/util/trailing_array.h +++ /dev/null @@ -1,29 +0,0 @@ -#pragma once - -// Copyright (c) Microsoft Corporation. All Rights Reserved. - -// Many classes in Z3 use the "trailing array" idiom: the last field -// of the class C is a zero-length array of some type T, and the allocation -// of an instance adds extra space for some number of T's (usually the -// number is held in some other field of C). - -// Zero-length arrays are non-standard, and provoke a warning in Clang -// when -Wzero-length-array is specified. This file introduces a macro -// for this idiom, which, for compilers that give a warning, disables -// the warning around the declaration. So far that's only Clang, -// but more could be added. - -#define STR_PRAGMA_FOR_TRAILING_ARRAY(x) _Pragma(#x) - -#ifdef __clang__ -#define TRAILING_ARRAY(type, field) \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic push) \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic ignored "-Wzero-length-array") \ - type field[0]; \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic pop) - -#else -#define TRAILING_ARRAY(type, field) type field[0]; - -#endif - From e5b5b2a83f89ad673fe94e736955d812a679dde2 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 11 Jun 2026 13:15:08 -0700 Subject: [PATCH 04/13] Undo previous changes; use a much simpler solution. --- cmake/compiler_warnings.cmake | 9 ++++++++- src/ast/ast.h | 7 +++---- src/ast/euf/euf_enode.h | 3 +-- src/ast/euf/euf_mam.cpp | 9 ++++----- src/ast/rewriter/cached_var_subst.h | 3 +-- src/ast/simplifiers/euf_completion.h | 3 +-- src/math/polynomial/polynomial.cpp | 3 +-- src/math/polynomial/rpolynomial.cpp | 3 +-- src/math/subpaving/subpaving_t.h | 5 ++--- src/muz/base/dl_rule.h | 3 +-- src/nlsat/nlsat_clause.h | 3 +-- src/nlsat/nlsat_interval_set.cpp | 3 +-- src/nlsat/nlsat_justification.h | 3 +-- src/nlsat/nlsat_types.h | 3 +-- src/sat/sat_clause.h | 3 +-- src/sat/sat_lookahead.h | 3 +-- src/sat/smt/ba_xor.h | 3 +-- src/sat/smt/pb_card.h | 3 +-- src/sat/smt/pb_pb.h | 3 +-- src/sat/smt/q_clause.h | 3 +-- src/sat/smt/q_solver.h | 3 +-- src/sat/smt/sat_smt.h | 3 +-- src/smt/mam.cpp | 9 ++++----- src/smt/smt_clause.h | 3 +-- src/smt/smt_enode.h | 3 +-- src/smt/smt_quantifier_instances.h | 3 +-- src/util/mpz.h | 3 +-- src/util/sexpr.cpp | 3 +-- src/util/trailing_array.h | 29 ---------------------------- 29 files changed, 44 insertions(+), 93 deletions(-) delete mode 100644 src/util/trailing_array.h diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 0f9e9d09a..d8dc90c05 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -9,10 +9,17 @@ set(GCC_ONLY_WARNINGS "") # Disable C++98 compatibility warnings to prevent excessive warning output # when building with clang-cl or when -Weverything is enabled. # These warnings are not useful for Z3 since it requires C++20. +# +# The "-Wno-zero-length-array" is for cases where Z3 is fetched by a CMake build +# to serve as a component in another system. Z3 has many classes whose last member +# is a zero-length array of some type T, indicating a variable-length array of T. +# If the including system compiles with "-Wzero-length-array", there will be +# many warnings. Overriding this prevents such warnings in the Z3 portion of the +# build of the including system. set(CLANG_ONLY_WARNINGS "-Wno-c++98-compat" "-Wno-c++98-compat-pedantic" - "-Wzero-length-array" + "-Wno-zero-length-array" ) set(MSVC_WARNINGS "/W3") diff --git a/src/ast/ast.h b/src/ast/ast.h index 0922ad759..03713ee4b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -20,7 +20,6 @@ Revision History: #include "util/vector.h" -#include "util/trailing_array.h" #include "util/hashtable.h" #include "util/buffer.h" #include "util/zstring.h" @@ -643,7 +642,7 @@ class func_decl : public decl { unsigned m_arity; sort * m_range; - TRAILING_ARRAY(sort *, m_domain); + sort * m_domain[0]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); } @@ -726,7 +725,7 @@ class app : public expr { func_decl * m_decl; unsigned m_num_args; app_flags m_flags; - TRAILING_ARRAY(expr *, m_args); + expr * m_args[0]; static unsigned get_obj_size(unsigned num_args) { return sizeof(app) + num_args * sizeof(expr *); @@ -873,7 +872,7 @@ class quantifier : public expr { symbol m_skid; unsigned m_num_patterns; unsigned m_num_no_patterns; - TRAILING_ARRAY(char, m_patterns_decls); + char m_patterns_decls[0]; static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*)); diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index b6bd5302a..af22a5b2c 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -16,7 +16,6 @@ Author: --*/ #include "util/vector.h" -#include "util/trailing_array.h" #include "util/id_var_list.h" #include "util/lbool.h" #include "util/approx_set.h" @@ -67,7 +66,7 @@ namespace euf { signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; - TRAILING_ARRAY(enode*, m_args); + enode* m_args[0]; friend class enode_args; friend class enode_parents; diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index 686b0d938..8148fe7d9 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -20,7 +20,6 @@ Revision History: --*/ #include -#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -232,7 +231,7 @@ namespace euf { The size of the array is m_num_args. */ - TRAILING_ARRAY(enode *, m_joints); + enode * m_joints[0]; }; struct bind : public instruction { @@ -248,21 +247,21 @@ namespace euf { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - TRAILING_ARRAY(unsigned, m_bindings); + unsigned m_bindings[0]; }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/ast/rewriter/cached_var_subst.h b/src/ast/rewriter/cached_var_subst.h index 530f57404..ad9364967 100644 --- a/src/ast/rewriter/cached_var_subst.h +++ b/src/ast/rewriter/cached_var_subst.h @@ -19,14 +19,13 @@ Revision History: #pragma once #include "ast/rewriter/var_subst.h" -#include "util/trailing_array.h" #include "util/map.h" class cached_var_subst { struct key { quantifier * m_qa; unsigned m_num_bindings; - TRAILING_ARRAY(expr *, m_bindings); + expr * m_bindings[0]; }; struct key_hash_proc { unsigned operator()(key * k) const { diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index 7076734ba..97fc45a42 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -21,7 +21,6 @@ Author: #pragma once #include "util/scoped_vector.h" -#include "util/trailing_array.h" #include "util/dlist.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/euf/euf_egraph.h" @@ -54,7 +53,7 @@ namespace euf { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - TRAILING_ARRAY(euf::enode*, m_nodes); + euf::enode* m_nodes[0]; binding(quantifier* q, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) : m_q(q), diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index b846d7da3..1b06fb2b0 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "math/polynomial/polynomial.h" -#include "util/trailing_array.h" #include "util/vector.h" #include "util/chashtable.h" #include "util/small_object_allocator.h" @@ -161,7 +160,7 @@ namespace polynomial { unsigned m_total_degree; //!< total degree of the monomial unsigned m_size; //!< number of powers unsigned m_hash; - TRAILING_ARRAY(power, m_powers); + power m_powers[0]; friend class tmp_monomial; void sort() { diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp index 181aaf64e..67b882525 100644 --- a/src/math/polynomial/rpolynomial.cpp +++ b/src/math/polynomial/rpolynomial.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "math/polynomial/rpolynomial.h" -#include "util/trailing_array.h" #include "util/tptr.h" #include "util/buffer.h" @@ -40,7 +39,7 @@ namespace rpolynomial { unsigned m_ref_count; var m_var; unsigned m_size; - TRAILING_ARRAY(poly_or_num *, m_args); + poly_or_num * m_args[0]; public: unsigned ref_count() const { return m_ref_count; } diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 3cf14da67..7300e3da3 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include -#include "util/trailing_array.h" #include "util/tptr.h" #include "util/small_object_allocator.h" #include "util/chashtable.h" @@ -95,7 +94,7 @@ public: unsigned m_lemma:1; //!< True if it is a learned clause. unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched. unsigned m_num_jst:30; //!< Number of times it is used to justify some bound. - TRAILING_ARRAY(ineq *, m_atoms); + ineq * m_atoms[0]; static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); } public: clause():constraint(constraint::CLAUSE) {} @@ -323,7 +322,7 @@ public: class monomial : public definition { friend class context_t; unsigned m_size; - TRAILING_ARRAY(power, m_powers); + power m_powers[0]; monomial(unsigned sz, power const * pws); static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); } public: diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 1b304454d..87c2637a9 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -20,7 +20,6 @@ Revision History: #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "muz/base/dl_costs.h" #include "muz/base/dl_util.h" #include "ast/used_vars.h" @@ -309,7 +308,7 @@ namespace datalog { The negated flag is never set for interpreted tails. */ - TRAILING_ARRAY(app *, m_tail); + app * m_tail[0]; static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h index 667f39bae..91467303c 100644 --- a/src/nlsat/nlsat_clause.h +++ b/src/nlsat/nlsat_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" -#include "util/trailing_array.h" #include "util/vector.h" namespace nlsat { @@ -35,7 +34,7 @@ namespace nlsat { unsigned m_marked:1; unsigned m_var_hash; assumption_set m_assumptions; - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } clause(unsigned id, unsigned sz, literal const * lits, bool learned, assumption_set as); diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 9f8a8d7cc..dc5740e10 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include "nlsat/nlsat_interval_set.h" -#include "util/trailing_array.h" #include "math/polynomial/algebraic_numbers.h" #include "util/buffer.h" @@ -40,7 +39,7 @@ namespace nlsat { unsigned m_num_intervals; unsigned m_ref_count:31; unsigned m_full:1; - TRAILING_ARRAY(interval, m_intervals); + interval m_intervals[0]; }; void display(std::ostream & out, anum_manager & am, interval const & curr) { diff --git a/src/nlsat/nlsat_justification.h b/src/nlsat/nlsat_justification.h index 9b1344298..d9567ebf9 100644 --- a/src/nlsat/nlsat_justification.h +++ b/src/nlsat/nlsat_justification.h @@ -20,7 +20,6 @@ Revision History: #pragma once #include "nlsat/nlsat_types.h" -#include "util/trailing_array.h" #include "util/tptr.h" namespace nlsat { @@ -39,7 +38,7 @@ namespace nlsat { class lazy_justification { unsigned m_num_literals; unsigned m_num_clauses; - TRAILING_ARRAY(char, m_data); + char m_data[0]; nlsat::clause* const* clauses() const { return (nlsat::clause *const*)(m_data); } public: static unsigned get_obj_size(unsigned nl, unsigned nc) { return sizeof(lazy_justification) + sizeof(literal)*nl + sizeof(nlsat::clause*)*nc; } diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index b79cb428c..be8f625c9 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "math/polynomial/polynomial.h" -#include "util/trailing_array.h" #include "util/buffer.h" #include "sat/sat_types.h" #include "util/z3_exception.h" @@ -100,7 +99,7 @@ namespace nlsat { class ineq_atom : public atom { friend class solver; unsigned m_size; - TRAILING_ARRAY(poly *, m_ps); + poly * m_ps[0]; ineq_atom(kind k, unsigned sz, poly * const * ps, bool const * is_even, var max_var); static unsigned get_obj_size(unsigned sz) { return sizeof(ineq_atom) + sizeof(poly*)*sz; } public: diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1635def8e..0129febbf 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "util/small_object_allocator.h" -#include "util/trailing_array.h" #include "util/id_gen.h" #include "util/map.h" #include "sat/sat_types.h" @@ -54,7 +53,7 @@ namespace sat { unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } size_t get_size() const { return get_obj_size(m_capacity); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 954a09fb4..87757ba59 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -21,7 +21,6 @@ Notes: #include "util/small_object_allocator.h" -#include "util/trailing_array.h" #include "sat/sat_elim_eqs.h" namespace pb { @@ -148,7 +147,7 @@ namespace sat { unsigned m_size; // number of non-false literals size_t m_obj_size; // object size (counting all literals) literal m_head; // head literal - TRAILING_ARRAY(literal, m_literals); // list of literals, put any true literal in head. + literal m_literals[0]; // list of literals, put any true literal in head. size_t num_lits() const { return (m_obj_size - sizeof(nary)) / sizeof(literal); } diff --git a/src/sat/smt/ba_xor.h b/src/sat/smt/ba_xor.h index b61e47c04..009534951 100644 --- a/src/sat/smt/ba_xor.h +++ b/src/sat/smt/ba_xor.h @@ -18,14 +18,13 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/ba_constraint.h" namespace ba { class xr : public constraint { - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(xr) + num_lits * sizeof(literal)); } xr(unsigned id, literal_vector const& lits); diff --git a/src/sat/smt/pb_card.h b/src/sat/smt/pb_card.h index 184b8259a..26c6d3bb1 100644 --- a/src/sat/smt/pb_card.h +++ b/src/sat/smt/pb_card.h @@ -18,14 +18,13 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/pb_constraint.h" namespace pb { class card : public constraint { - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(card) + num_lits * sizeof(literal)); } card(unsigned id, literal lit, literal_vector const& lits, unsigned k); diff --git a/src/sat/smt/pb_pb.h b/src/sat/smt/pb_pb.h index 7e020afaa..5386051af 100644 --- a/src/sat/smt/pb_pb.h +++ b/src/sat/smt/pb_pb.h @@ -18,7 +18,6 @@ Author: #pragma once #include "sat/sat_types.h" -#include "util/trailing_array.h" #include "sat/smt/pb_card.h" @@ -28,7 +27,7 @@ namespace pb { unsigned m_slack; unsigned m_num_watch; unsigned m_max_sum; - TRAILING_ARRAY(wliteral, m_wlits); + wliteral m_wlits[0]; public: static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(pbc) + num_lits * sizeof(wliteral)); } pbc(unsigned id, literal lit, svector const& wlits, unsigned k); diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 0fb3636cb..aedb0bc4c 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -17,7 +17,6 @@ Author: #pragma once #include "util/dlist.h" -#include "util/trailing_array.h" #include "ast/ast.h" #include "ast/quantifier_stat.h" #include "ast/euf/euf_enode.h" @@ -67,7 +66,7 @@ namespace q { unsigned m_max_generation; unsigned m_min_top_generation; unsigned m_max_top_generation; - TRAILING_ARRAY(euf::enode*, m_nodes); + euf::enode* m_nodes[0]; binding(clause& c, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top): c(&c), diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 40b8195a7..a7220e68b 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -17,7 +17,6 @@ Author: #pragma once #include "util/obj_hashtable.h" -#include "util/trailing_array.h" #include "ast/ast_trail.h" #include "ast/rewriter/der.h" #include "sat/smt/sat_th.h" @@ -36,7 +35,7 @@ namespace q { unsigned m_num_bindings; unsigned m_num_literals; sat::literal* m_literals; - TRAILING_ARRAY(expr*, m_bindings); + expr* m_bindings[0]; q_proof_hint(symbol const& method, unsigned g, unsigned b, unsigned l) { m_method = method; diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 51134d6df..c661288f5 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -16,7 +16,6 @@ Author: --*/ #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/sat_solver.h" @@ -32,7 +31,7 @@ namespace sat { class constraint_base { extension* m_ex = nullptr; - TRAILING_ARRAY(unsigned, m_mem); + unsigned m_mem[0]; static size_t ext_size() { return sizeof(((constraint_base*)nullptr)->m_ex); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index aa04851a4..80918fcb4 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include -#include "util/trailing_array.h" #include "util/pool.h" #include "util/trail.h" @@ -208,7 +207,7 @@ namespace { The size of the array is m_num_args. */ - TRAILING_ARRAY(enode *, m_joints); + enode * m_joints[0]; }; struct bind : public instruction { @@ -224,21 +223,21 @@ namespace { approx_set m_lbl_set; unsigned short m_num_args; unsigned m_oreg; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; struct yield : public instruction { quantifier * m_qa; app * m_pat; unsigned short m_num_bindings; - TRAILING_ARRAY(unsigned, m_bindings); + unsigned m_bindings[0]; }; struct is_cgr : public instruction { unsigned m_ireg; func_decl * m_label; unsigned short m_num_args; - TRAILING_ARRAY(unsigned, m_iregs); + unsigned m_iregs[0]; }; void display_num_args(std::ostream & out, unsigned num_args) { diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index c1f50edcb..89d8f2d66 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "ast/ast.h" -#include "util/trailing_array.h" #include "smt/smt_literal.h" #include "util/tptr.h" #include "util/obj_hashtable.h" @@ -63,7 +62,7 @@ namespace smt { unsigned m_has_del_eh:1; //!< true if must notify event handler when deleted. unsigned m_has_justification:1; //!< true if the clause has a justification attached to it. unsigned m_deleted:1; //!< true if the clause is marked for deletion by was not deleted yet because it is referenced by some data-structure (e.g., m_lemmas) - TRAILING_ARRAY(literal, m_lits); + literal m_lits[0]; static unsigned get_obj_size(unsigned num_lits, clause_kind k, bool has_atoms, bool has_del_eh, bool has_justification) { unsigned r = sizeof(clause) + sizeof(literal) * num_lits; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 84ffe9def..e9dc4c4e1 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include "util/id_var_list.h" -#include "util/trailing_array.h" #include "util/approx_set.h" #include "ast/ast.h" #include "ast/ast_pp.h" @@ -102,7 +101,7 @@ namespace smt { trans_justification m_trans; //!< A justification for the enode being equal to its root. approx_set m_lbls; approx_set m_plbls; - TRAILING_ARRAY(enode *, m_args); //!< Cached args + enode * m_args[0]; //!< Cached args friend class context; friend class conflict_resolution; diff --git a/src/smt/smt_quantifier_instances.h b/src/smt/smt_quantifier_instances.h index d8b95f807..6bd76a335 100644 --- a/src/smt/smt_quantifier_instances.h +++ b/src/smt/smt_quantifier_instances.h @@ -1,4 +1,3 @@ -#include "util/trailing_array.h" /*++ Copyright (c) 2006 Microsoft Corporation @@ -26,7 +25,7 @@ namespace smt { class quantifier_instance { quantifier * m_quantifier; double m_cost; - TRAILING_ARRAY(enode *, m_enodes); + enode * m_enodes[0]; quantifier_instance(quantifier * q, enode * const * enodes); friend class quantifier_instances; public: diff --git a/src/util/mpz.h b/src/util/mpz.h index 7aa85ed24..7b714b9be 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -19,7 +19,6 @@ Revision History: #pragma once #include -#include "util/trailing_array.h" #include "util/mutex.h" #include "util/util.h" #include "util/small_object_allocator.h" @@ -58,7 +57,7 @@ typedef unsigned int digit_t; class mpz_cell { unsigned m_size; unsigned m_capacity; - TRAILING_ARRAY(digit_t, m_digits); + digit_t m_digits[0]; friend class mpz_manager; friend class mpz_manager; friend class mpz_stack; diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index bc2cd3295..4b0b8378d 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "util/sexpr.h" -#include "util/trailing_array.h" #include "util/vector.h" #include "util/buffer.h" @@ -28,7 +27,7 @@ Notes: struct sexpr_composite : public sexpr { unsigned m_num_children; - TRAILING_ARRAY(sexpr *, m_children); + sexpr * m_children[0]; sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos): sexpr(kind_t::COMPOSITE, line, pos), m_num_children(num_children) { diff --git a/src/util/trailing_array.h b/src/util/trailing_array.h deleted file mode 100644 index aecfec974..000000000 --- a/src/util/trailing_array.h +++ /dev/null @@ -1,29 +0,0 @@ -#pragma once - -// Copyright (c) Microsoft Corporation. All Rights Reserved. - -// Many classes in Z3 use the "trailing array" idiom: the last field -// of the class C is a zero-length array of some type T, and the allocation -// of an instance adds extra space for some number of T's (usually the -// number is held in some other field of C). - -// Zero-length arrays are non-standard, and provoke a warning in Clang -// when -Wzero-length-array is specified. This file introduces a macro -// for this idiom, which, for compilers that give a warning, disables -// the warning around the declaration. So far that's only Clang, -// but more could be added. - -#define STR_PRAGMA_FOR_TRAILING_ARRAY(x) _Pragma(#x) - -#ifdef __clang__ -#define TRAILING_ARRAY(type, field) \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic push) \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic ignored "-Wzero-length-array") \ - type field[0]; \ - STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic pop) - -#else -#define TRAILING_ARRAY(type, field) type field[0]; - -#endif - From 639530f42a8eccaeb2cce6c40b2a4fa608e21f5d Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Mon, 15 Jun 2026 13:46:51 -0700 Subject: [PATCH 05/13] Remove unused private fields and local vars. --- src/ast/simplifiers/dependent_expr_state.h | 2 +- src/smt/smt_context.cpp | 1 - src/smt/theory_sls.h | 1 - src/solver/parallel_tactical2.cpp | 3 +-- 4 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 504f67ad0..ed34d4a19 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -45,7 +45,7 @@ Author: class dependent_expr_state { unsigned m_qhead = 0; bool m_suffix_frozen = false; - unsigned m_num_recfun = 0, m_num_lambdas = 0; + unsigned m_num_recfun = 0; lbool m_has_quantifiers = l_undef; ast_mark m_frozen; func_decl_ref_vector m_frozen_trail; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 098240fc9..c23da2bba 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4672,7 +4672,6 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - auto p = parent->get_expr(); family_id fid = parent->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index 2b65783b4..856f8f3d2 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -66,7 +66,6 @@ namespace smt { unsigned m_final_check_ls_steps = 30000; unsigned m_final_check_ls_steps_delta = 10000; unsigned m_final_check_ls_steps_min = 10000; - unsigned m_final_check_ls_steps_max = 30000; bool m_has_unassigned_clause_after_resolve = false; unsigned m_after_resolve_decide_gap = 4; unsigned m_after_resolve_decide_count = 0; diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..dffb5f15c 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -460,7 +460,6 @@ class parallel_solver { }; unsigned id; - parallel_solver& p; batch_manager& b; ast_manager m; /* worker-local manager */ ref s; /* translated solver copy */ @@ -579,7 +578,7 @@ class parallel_solver { worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, expr_ref_vector const& src_asms) - : id(id), p(p), b(p.m_batch_manager), + : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { /* create translated solver copy */ From 8eff8eb119f7e1bd6e83f92b2d54deca03d2b07d Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Tue, 16 Jun 2026 13:42:46 -0700 Subject: [PATCH 06/13] Fix "flexible array members" warning. --- src/model/func_interp.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/func_interp.h b/src/model/func_interp.h index e531e01cf..e3935e05e 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -40,7 +40,7 @@ class func_entry { // m_result and m_args[i] must be ground terms. expr * m_result; - expr * m_args[]; + expr * m_args[0]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); } func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result); From 7ce5b687fab4de66f2d6c213df0ffefe4282ada5 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Wed, 17 Jun 2026 08:29:36 -0700 Subject: [PATCH 07/13] Fix "override"-related warnings. --- src/cmd_context/cmd_util.h | 68 ++++++++++++----------- src/math/lp/dioph_eq.cpp | 2 +- src/math/lp/static_matrix.h | 10 ++-- src/solver/assertions/asserted_formulas.h | 10 ++-- 4 files changed, 48 insertions(+), 42 deletions(-) diff --git a/src/cmd_context/cmd_util.h b/src/cmd_context/cmd_util.h index 125ed6654..19c6e47fb 100644 --- a/src/cmd_context/cmd_util.h +++ b/src/cmd_context/cmd_util.h @@ -17,45 +17,51 @@ Notes: --*/ #pragma once -#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION) \ +#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION) \ +class CLS_NAME : public cmd { \ +public: \ + CLS_NAME():cmd(NAME) {} \ + char const * get_usage() const override { return 0; } \ + char const * get_descr(cmd_context & ctx) const override { \ + return DESCR; \ + } \ + unsigned get_arity() const override { return 0; } \ + void execute(cmd_context & ctx) override { ACTION } \ +} + +#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \ class CLS_NAME : public cmd { \ public: \ CLS_NAME():cmd(NAME) {} \ - virtual char const * get_usage() const { return 0; } \ - virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \ - virtual unsigned get_arity() const { return 0; } \ - virtual void execute(cmd_context & ctx) { ACTION } \ -}; - -#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \ -class CLS_NAME : public cmd { \ -public: \ - CLS_NAME():cmd(NAME) {} \ - virtual char const * get_usage() const { return USAGE; } \ - virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \ - virtual unsigned get_arity() const { return 1; } \ - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return ARG_KIND; } \ - virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION } \ + char const * get_usage() const override { return USAGE; } \ + char const * get_descr(cmd_context & ctx) const override { \ + return DESCR; \ + } \ + unsigned get_arity() const override { return 1; } \ + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \ + return ARG_KIND; \ + } \ + void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \ } // Macro for creating commands where the first argument is a symbol // The second argument cannot be a symbol #define BINARY_SYM_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \ -class CLS_NAME : public cmd { \ - symbol m_sym; \ -public: \ - CLS_NAME():cmd(NAME) {} \ - virtual char const * get_usage() const { return USAGE; } \ - virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \ - virtual unsigned get_arity() const { return 2; } \ - virtual void prepare(cmd_context & ctx) { m_sym = symbol::null; } \ - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { \ - return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \ - } \ - virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_sym = s; } \ - virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION } \ -}; - +class CLS_NAME : public cmd { \ + symbol m_sym; \ +public: \ + CLS_NAME():cmd(NAME) {} \ + char const * get_usage() const override { return USAGE; } \ + char const * get_descr(cmd_context & ctx) const override { return DESCR; } \ + unsigned get_arity() const override { return 2; } \ + void prepare(cmd_context & ctx) override { m_sym = symbol::null; } \ + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \ + return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \ + } \ + void set_next_arg(cmd_context & ctx, symbol const & s) override { m_sym = s; } \ + void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \ +} + class ast; class expr; diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 0b3c5166a..c6719e0e3 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -580,7 +580,7 @@ namespace lp { const lar_term* m_t; undo_add_term(imp& s, const lar_term* t) : m_s(s), m_t(t) {} - void undo() { + void undo() override { m_s.undo_add_term_method(m_t); } }; diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 08db2245d..5395bf44f 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -119,9 +119,9 @@ public: void init_empty_matrix(unsigned m, unsigned n); - unsigned row_count() const { return static_cast(m_rows.size()); } + unsigned row_count() const override { return static_cast(m_rows.size()); } - unsigned column_count() const { return static_cast(m_columns.size()); } + unsigned column_count() const override { return static_cast(m_columns.size()); } unsigned lowest_row_in_column(unsigned col); @@ -197,7 +197,7 @@ public: void cross_out_row_from_column(unsigned col, unsigned k); - T get_elem(unsigned i, unsigned j) const; + T get_elem(unsigned i, unsigned j) const override; unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast(m_columns[j].size()); } @@ -218,8 +218,8 @@ public: #ifdef Z3DEBUG unsigned get_number_of_rows() const { return row_count(); } unsigned get_number_of_columns() const { return column_count(); } - virtual void set_number_of_rows(unsigned /*m*/) { } - virtual void set_number_of_columns(unsigned /*n*/) { } + void set_number_of_rows(unsigned /*m*/) override { } + void set_number_of_columns(unsigned /*n*/) override { } #endif T get_balance() const; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 262499ff4..ba0b1f840 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -185,12 +185,12 @@ class asserted_formulas { public: \ FUNCTOR m_functor; \ NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \ - virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \ - m_functor(j.fml(), n, p); \ + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { \ + m_functor(j.fml(), n, p); \ } \ - virtual void post_op() { if (REDUCE) af.reduce_and_solve(); } \ - virtual bool should_apply() const { return APP; } \ - }; \ + void post_op() override { if (REDUCE) af.reduce_and_solve(); } \ + bool should_apply() const override { return APP; } \ + }; #define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE) From 360bad9a3514d0db4c87478e6b5366e20391288f Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Wed, 17 Jun 2026 08:33:55 -0700 Subject: [PATCH 08/13] Remove tabs in macro; for some reason changes in compiler_warnings wasn't included. --- src/cmd_context/cmd_util.h | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cmd_context/cmd_util.h b/src/cmd_context/cmd_util.h index 19c6e47fb..cec79a26f 100644 --- a/src/cmd_context/cmd_util.h +++ b/src/cmd_context/cmd_util.h @@ -47,19 +47,19 @@ public: // Macro for creating commands where the first argument is a symbol // The second argument cannot be a symbol #define BINARY_SYM_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \ -class CLS_NAME : public cmd { \ - symbol m_sym; \ -public: \ - CLS_NAME():cmd(NAME) {} \ - char const * get_usage() const override { return USAGE; } \ - char const * get_descr(cmd_context & ctx) const override { return DESCR; } \ - unsigned get_arity() const override { return 2; } \ - void prepare(cmd_context & ctx) override { m_sym = symbol::null; } \ - cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \ - return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \ - } \ - void set_next_arg(cmd_context & ctx, symbol const & s) override { m_sym = s; } \ - void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \ +class CLS_NAME : public cmd { \ + symbol m_sym; \ +public: \ + CLS_NAME():cmd(NAME) {} \ + char const * get_usage() const override { return USAGE; } \ + char const * get_descr(cmd_context & ctx) const override { return DESCR; } \ + unsigned get_arity() const override { return 2; } \ + void prepare(cmd_context & ctx) override { m_sym = symbol::null; } \ + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \ + return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \ + } \ + void set_next_arg(cmd_context & ctx, symbol const & s) override { m_sym = s; } \ + void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \ } From abaa46aa885d4aefb6ff97e986cd80034b66c327 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Wed, 17 Jun 2026 08:37:23 -0700 Subject: [PATCH 09/13] Oops: wasn't including compiler_warnings because I wasn't doing git add from base directory. --- cmake/compiler_warnings.cmake | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index d8dc90c05..38b442e83 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -20,6 +20,9 @@ set(CLANG_ONLY_WARNINGS "-Wno-c++98-compat" "-Wno-c++98-compat-pedantic" "-Wno-zero-length-array" + "-Wc99-extensions" + "-Wsuggest-override" + "-Winconsistent-missing-override" ) set(MSVC_WARNINGS "/W3") From 8cb5f32ef7bc3263b95e9b09f549dc702e71e1fd Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 18 Jun 2026 09:16:25 -0700 Subject: [PATCH 10/13] Some of the overrides are only in debug builds; handle this. --- src/math/lp/static_matrix.h | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 5395bf44f..c04728cc8 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -60,6 +60,14 @@ std::ostream& operator<<(std::ostream& out, const row_strip& r) { return out << "\n"; } +// Below, static_matrix has a superclass when Z3DEBUG is set, and some +// methods are overrides in that case. +#ifdef Z3DEBUG +#define DEBUG_OVERRIDE override +#else +#define DEBUG_OVERRIDE +#endif + // each assignment for this matrix should be issued only once!!! template class static_matrix @@ -119,9 +127,13 @@ public: void init_empty_matrix(unsigned m, unsigned n); - unsigned row_count() const override { return static_cast(m_rows.size()); } + unsigned row_count() const DEBUG_OVERRIDE { + return static_cast(m_rows.size()); + } - unsigned column_count() const override { return static_cast(m_columns.size()); } + unsigned column_count() const DEBUG_OVERRIDE { + return static_cast(m_columns.size()); + } unsigned lowest_row_in_column(unsigned col); @@ -197,7 +209,7 @@ public: void cross_out_row_from_column(unsigned col, unsigned k); - T get_elem(unsigned i, unsigned j) const override; + T get_elem(unsigned i, unsigned j) const DEBUG_OVERRIDE; unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast(m_columns[j].size()); } From 75b81900d55bbde9d4859f5cf552f09c71fbdff1 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 18 Jun 2026 19:22:05 -0700 Subject: [PATCH 11/13] Fix "missing field initializer" warnings. --- cmake/compiler_warnings.cmake | 1 + src/util/map.h | 10 +++++----- src/util/obj_hashtable.h | 19 ++++++++++++------- src/util/symbol_table.h | 8 ++++++-- 4 files changed, 24 insertions(+), 14 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 38b442e83..f6529c21a 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -23,6 +23,7 @@ set(CLANG_ONLY_WARNINGS "-Wc99-extensions" "-Wsuggest-override" "-Winconsistent-missing-override" + "-Wmissing-field-initializers" ) set(MSVC_WARNINGS "/W3") diff --git a/src/util/map.h b/src/util/map.h index fb72db01f..f6fe38ec2 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -115,7 +115,7 @@ public: } entry * find_core(key const & k) const { - return m_table.find_core(key_data{k}); + return m_table.find_core(key_data{k, value()}); } bool find(key const & k, value & v) const { @@ -137,7 +137,7 @@ public: } iterator find_iterator(key const & k) const { - return m_table.find(key_data{k}); + return m_table.find(key_data{k, value()}); } value const & find(key const& k) const { @@ -161,10 +161,10 @@ public: return find_core(k) != nullptr; } - void remove(key const & k) { - m_table.remove(key_data{k}); + void remove(key const &k) { + m_table.remove(key_data{k, value()}); } - + void erase(key const & k) { remove(k); } diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 0b39163ea..ae2a54f04 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -62,6 +62,11 @@ public: struct key_data { Key * m_key = nullptr; Value m_value; + + key_data() : m_key(nullptr), m_value(Value()) {} + key_data(Key * key) : m_key(key), m_value(Value()) {} + key_data(Key * key, const Value& value) : m_key(key), m_value(value) {} + Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } @@ -156,8 +161,8 @@ public: obj_map_entry * insert_if_not_there3(Key * k, Value const & v) { return m_table.insert_if_not_there2({k, v}); } - - obj_map_entry * find_core(Key * k) const { + + obj_map_entry *find_core(Key *k) const { return m_table.find_core({k}); } @@ -188,8 +193,8 @@ public: value & operator[](key * k) { return find(k); } - - iterator find_iterator(Key * k) const { + + iterator find_iterator(Key *k) const { return m_table.find(key_data{k}); } @@ -197,10 +202,10 @@ public: return find_core(k) != nullptr; } - void remove(Key * k) { - m_table.remove(key_data{k}); + void remove(Key *k) { + m_table.remove(key_data{k, value()}); } - + void erase(Key * k) { remove(k); } diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index c6dbb9f82..079f6357c 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -30,6 +30,10 @@ class symbol_table { struct key_data { symbol m_key; T m_data; + + key_data() {} + key_data(const symbol &key) : m_key(key) {} + key_data(const symbol &key, const T &data) : m_key(key), m_data(data) {} }; struct key_data_hash_proc { @@ -116,8 +120,8 @@ public: result = e->get_data().m_data; return true; } - - bool contains(symbol key) const { + + bool contains(symbol key) const { return m_sym_table.contains(key_data{key}); } From d6d0d4e45ad84695e7e304713cf2315e6a6f2191 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 18 Jun 2026 19:36:55 -0700 Subject: [PATCH 12/13] Fix inadvertent formatting changes. --- src/util/map.h | 10 +++++----- src/util/obj_hashtable.h | 8 ++++---- src/util/symbol_table.h | 6 +++--- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/util/map.h b/src/util/map.h index f6fe38ec2..849c3d24a 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -115,7 +115,7 @@ public: } entry * find_core(key const & k) const { - return m_table.find_core(key_data{k, value()}); + return m_table.find_core(key_data{k, value{}}); } bool find(key const & k, value & v) const { @@ -137,7 +137,7 @@ public: } iterator find_iterator(key const & k) const { - return m_table.find(key_data{k, value()}); + return m_table.find(key_data{k, value{}}); } value const & find(key const& k) const { @@ -161,8 +161,8 @@ public: return find_core(k) != nullptr; } - void remove(key const &k) { - m_table.remove(key_data{k, value()}); + void remove(key const & k) { + m_table.remove(key_data{k, value{}}); } void erase(key const & k) { @@ -184,7 +184,7 @@ public: } return true; } - + #ifdef Z3DEBUG bool check_invariant() { diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index ae2a54f04..e158d09cb 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -65,7 +65,7 @@ public: key_data() : m_key(nullptr), m_value(Value()) {} key_data(Key * key) : m_key(key), m_value(Value()) {} - key_data(Key * key, const Value& value) : m_key(key), m_value(value) {} + key_data(Key * key, const Value & value) : m_key(key), m_value(value) {} Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } @@ -162,7 +162,7 @@ public: return m_table.insert_if_not_there2({k, v}); } - obj_map_entry *find_core(Key *k) const { + obj_map_entry *find_core(Key * k) const { return m_table.find_core({k}); } @@ -194,7 +194,7 @@ public: return find(k); } - iterator find_iterator(Key *k) const { + iterator find_iterator(Key * k) const { return m_table.find(key_data{k}); } @@ -202,7 +202,7 @@ public: return find_core(k) != nullptr; } - void remove(Key *k) { + void remove(Key * k) { m_table.remove(key_data{k, value()}); } diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 079f6357c..59301f4b2 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -32,8 +32,8 @@ class symbol_table { T m_data; key_data() {} - key_data(const symbol &key) : m_key(key) {} - key_data(const symbol &key, const T &data) : m_key(key), m_data(data) {} + key_data(const symbol & key) : m_key(key) {} + key_data(const symbol & key, const T & data) : m_key(key), m_data(data) {} }; struct key_data_hash_proc { @@ -120,7 +120,7 @@ public: result = e->get_data().m_data; return true; } - + bool contains(symbol key) const { return m_sym_table.contains(key_data{key}); } From 9a0272528aad066832a300121258e62a5f24afd0 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 18 Jun 2026 19:40:53 -0700 Subject: [PATCH 13/13] Fix more inadvertent formatting changes. --- src/util/map.h | 6 +++--- src/util/obj_hashtable.h | 10 +++++----- src/util/symbol_table.h | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/util/map.h b/src/util/map.h index 849c3d24a..e45881fff 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -115,7 +115,7 @@ public: } entry * find_core(key const & k) const { - return m_table.find_core(key_data{k, value{}}); + return m_table.find_core(key_data{k, value{}}); } bool find(key const & k, value & v) const { @@ -164,7 +164,7 @@ public: void remove(key const & k) { m_table.remove(key_data{k, value{}}); } - + void erase(key const & k) { remove(k); } @@ -184,7 +184,7 @@ public: } return true; } - + #ifdef Z3DEBUG bool check_invariant() { diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index e158d09cb..3465c91fc 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -161,8 +161,8 @@ public: obj_map_entry * insert_if_not_there3(Key * k, Value const & v) { return m_table.insert_if_not_there2({k, v}); } - - obj_map_entry *find_core(Key * k) const { + + obj_map_entry * find_core(Key * k) const { return m_table.find_core({k}); } @@ -193,8 +193,8 @@ public: value & operator[](key * k) { return find(k); } - - iterator find_iterator(Key * k) const { + + iterator find_iterator(Key * k) const { return m_table.find(key_data{k}); } @@ -203,7 +203,7 @@ public: } void remove(Key * k) { - m_table.remove(key_data{k, value()}); + m_table.remove(key_data{k, value{}}); } void erase(Key * k) { diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 59301f4b2..47026e4eb 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -121,7 +121,7 @@ public: return true; } - bool contains(symbol key) const { + bool contains(symbol key) const { return m_sym_table.contains(key_data{key}); }