Undo previous changes; use a much simpler solution.

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")
 

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*));

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;

src/ast/euf/euf_mam.cpp

@@ -20,7 +20,6 @@ Revision History:
 
 --*/
 #include <algorithm>
-#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) {

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 {

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),

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() {

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; }

src/math/subpaving/subpaving_t.h

@@ -19,7 +19,6 @@ Revision History:
 #pragma once
 
 #include<ostream>
-#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:

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 *); }
 

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);

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) {

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; }

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:

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); }

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);
             }

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);

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);

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<wliteral> const& wlits, unsigned k);

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),

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;

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);
         }

src/smt/mam.cpp

@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include <algorithm>
-#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) {

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;

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;

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:

src/util/mpz.h

@@ -19,7 +19,6 @@ Revision History:
 #pragma once
 
 #include<string>
-#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<true>;
     friend class mpz_manager<false>;
     friend class mpz_stack;

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) {

src/util/trailing_array.h

@@ -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
-