From 35b0b42d2e737311cf16945a889cef5829d2a39f Mon Sep 17 00:00:00 2001 From: davedets Date: Wed, 22 Jul 2026 18:01:50 -0700 Subject: [PATCH] Use macros to disable semi-colon warnings for blocks of macros. (#10192) This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. This PR completes the job started by https://github.com/Z3Prover/z3/pull/10169. It adds `-Wextra-semi` to the set of CLANG_ONLY_WARNINGS, and adds ``` START_DISABLE_EXTRA_SEMI_WARNING; ...macro invocations with trailing semis... END_DISABLE_WARNING; ``` around all the blocks of macro invocations that provoked warnings. (Additionally, in realclosure.h, there was one block of macro invocations that did *not* follow the trailing-semi pattern; changed that to look like all the others). --- src/api/api_arith.cpp | 7 +++++++ src/api/api_array.cpp | 3 +++ src/api/api_ast.cpp | 3 +++ src/api/api_bv.cpp | 5 +++++ src/api/api_seq.cpp | 5 +++++ src/api/api_special_relations.cpp | 5 +++++ src/ast/arith_decl_plugin.h | 2 ++ src/ast/array_decl_plugin.h | 3 +++ src/ast/bv_decl_plugin.h | 2 ++ src/ast/char_decl_plugin.h | 3 +++ src/ast/datatype_decl_plugin.h | 5 +++++ src/ast/finite_set_decl_plugin.h | 3 +++ src/ast/fpa_decl_plugin.h | 3 +++ .../rewriter/bit_blaster/bit_blaster_rewriter.cpp | 11 +++++++++++ src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 3 +++ src/ast/rewriter/bv_rewriter.h | 3 +++ src/ast/rewriter/seq_skolem.h | 3 +++ src/ast/seq_decl_plugin.h | 7 +++++++ src/cmd_context/tactic_cmds.cpp | 5 +++++ src/math/polynomial/algebraic_numbers.h | 3 +++ src/math/realclosure/realclosure.h | 13 +++++++++---- src/smt/theory_bv.cpp | 7 +++++++ src/tactic/arith/bv2real_rewriter.h | 3 +++ src/util/manage_warnings.h | 2 +- src/util/mpbq.h | 3 +++ 25 files changed, 107 insertions(+), 5 deletions(-) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 806f720b32..46a22a516f 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -21,6 +21,7 @@ Revision History: #include "api/api_util.h" #include "ast/arith_decl_plugin.h" #include "math/polynomial/algebraic_numbers.h" +#include "util/manage_warnings.h" #include @@ -76,11 +77,13 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_ARITH_OP(Z3_mk_add, OP_ADD); MK_ARITH_OP(Z3_mk_mul, OP_MUL); MK_BINARY_ARITH_OP(Z3_mk_power, OP_POWER); MK_BINARY_ARITH_OP(Z3_mk_mod, OP_MOD); MK_BINARY_ARITH_OP(Z3_mk_rem, OP_REM); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast n1, Z3_ast n2) { Z3_TRY; @@ -100,10 +103,12 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_ARITH_PRED(Z3_mk_lt, OP_LT); MK_ARITH_PRED(Z3_mk_gt, OP_GT); MK_ARITH_PRED(Z3_mk_le, OP_LE); MK_ARITH_PRED(Z3_mk_ge, OP_GE); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast n1, Z3_ast n2) { Z3_TRY; @@ -123,10 +128,12 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP); MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP); MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP); MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]) { Z3_TRY; diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index 6b454530ea..fc34f0f675 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -20,6 +20,7 @@ Revision History: #include "api/api_context.h" #include "api/api_util.h" #include "ast/array_decl_plugin.h" +#include "util/manage_warnings.h" extern "C" { @@ -266,12 +267,14 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_NARY(Z3_mk_set_union, mk_c(c)->get_array_fid(), OP_SET_UNION, SKIP); MK_NARY(Z3_mk_set_intersect, mk_c(c)->get_array_fid(), OP_SET_INTERSECT, SKIP); MK_BINARY(Z3_mk_set_difference, mk_c(c)->get_array_fid(), OP_SET_DIFFERENCE, SKIP); MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP); MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP); MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) { Z3_TRY; diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index e98104e1b4..799623b79e 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -39,6 +39,7 @@ Revision History: #include "util/scoped_ctrl_c.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" +#include "util/manage_warnings.h" #include "ast/pp_params.hpp" #include "ast/expr_abstract.h" @@ -297,6 +298,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_UNARY(Z3_mk_not, mk_c(c)->get_basic_fid(), OP_NOT, SKIP); MK_BINARY(Z3_mk_eq, mk_c(c)->get_basic_fid(), OP_EQ, SKIP); MK_NARY(Z3_mk_distinct, mk_c(c)->get_basic_fid(), OP_DISTINCT, SKIP); @@ -305,6 +307,7 @@ extern "C" { MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP); MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP); MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP); + END_DISABLE_WARNING; Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) { expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3)); diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 77e7bfbc29..2f086e6dac 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -20,6 +20,7 @@ Revision History: #include "api/api_context.h" #include "api/api_util.h" #include "ast/bv_decl_plugin.h" +#include "util/manage_warnings.h" extern "C" { @@ -36,6 +37,7 @@ extern "C" { #define MK_BV_UNARY(NAME, OP) MK_UNARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) #define MK_BV_BINARY(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) + START_DISABLE_EXTRA_SEMI_WARNING; MK_BV_UNARY(Z3_mk_bvnot, OP_BNOT); MK_BV_UNARY(Z3_mk_bvredand, OP_BREDAND); MK_BV_UNARY(Z3_mk_bvredor, OP_BREDOR); @@ -66,6 +68,7 @@ extern "C" { MK_BV_BINARY(Z3_mk_bvashr, OP_BASHR); MK_BV_BINARY(Z3_mk_ext_rotate_left, OP_EXT_ROTATE_LEFT); MK_BV_BINARY(Z3_mk_ext_rotate_right, OP_EXT_ROTATE_RIGHT); + END_DISABLE_WARNING; static Z3_ast mk_extract_core(Z3_context c, unsigned high, unsigned low, Z3_ast n) { expr * _n = to_expr(n); @@ -99,6 +102,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_CATCH_RETURN(0); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_BV_PUNARY(Z3_mk_sign_ext, OP_SIGN_EXT); MK_BV_PUNARY(Z3_mk_zero_ext, OP_ZERO_EXT); MK_BV_PUNARY(Z3_mk_repeat, OP_REPEAT); @@ -106,6 +110,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ MK_BV_PUNARY(Z3_mk_rotate_left, OP_ROTATE_LEFT); MK_BV_PUNARY(Z3_mk_rotate_right, OP_ROTATE_RIGHT); MK_BV_PUNARY(Z3_mk_int2bv, OP_INT2BV); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, bool is_signed) { Z3_TRY; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 94756cc584..c003281faa 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -21,6 +21,7 @@ Revision History: #include "api/api_context.h" #include "api/api_util.h" #include "ast/ast_pp.h" +#include "util/manage_warnings.h" extern "C" { @@ -287,6 +288,7 @@ extern "C" { Z3_CATCH_RETURN(0); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty); MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP); @@ -316,6 +318,7 @@ extern "C" { MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP); MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP); MK_UNARY(Z3_mk_sbv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_SBVTOS, SKIP); + END_DISABLE_WARNING; Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { @@ -343,6 +346,7 @@ extern "C" { } + START_DISABLE_EXTRA_SEMI_WARNING; MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP); MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); @@ -367,6 +371,7 @@ extern "C" { MK_TERNARY(Z3_mk_seq_mapi, mk_c(c)->get_seq_fid(), OP_SEQ_MAPI, SKIP); MK_TERNARY(Z3_mk_seq_foldl, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDL, SKIP); MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP); + END_DISABLE_WARNING; } diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp index 0063fe7863..6257c37503 100644 --- a/src/api/api_special_relations.cpp +++ b/src/api/api_special_relations.cpp @@ -23,6 +23,7 @@ Revision History: #include "api/api_util.h" #include "ast/ast_pp.h" #include "ast/special_relations_decl_plugin.h" +#include "util/manage_warnings.h" extern "C" { @@ -39,10 +40,12 @@ extern "C" { Z3_CATCH_RETURN(nullptr); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_SPECIAL_R(Z3_mk_linear_order, OP_SPECIAL_RELATION_LO); MK_SPECIAL_R(Z3_mk_partial_order, OP_SPECIAL_RELATION_PO); MK_SPECIAL_R(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO); MK_SPECIAL_R(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO); + END_DISABLE_WARNING; #define MK_DECL(NAME, FID) \ @@ -60,5 +63,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC); + END_DISABLE_WARNING; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index cfad378a17..6529d6e3a2 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -346,6 +346,7 @@ public: is_pi(n); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_uminus); MATCH_UNARY(is_to_real); MATCH_UNARY(is_to_int); @@ -378,6 +379,7 @@ public: MATCH_UNARY(is_tan); MATCH_UNARY(is_atan); MATCH_UNARY(is_atanh); + END_DISABLE_WARNING; }; diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 0c4983eec2..0a888b8502 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "ast/ast.h" +#include "util/manage_warnings.h" inline sort* get_array_range(sort const * s) { @@ -207,7 +208,9 @@ public: } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_BINARY(is_subset); + END_DISABLE_WARNING; }; class array_util : public array_recognizers { diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 8900c53d0a..2d769fc9d6 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -390,6 +390,7 @@ public: return is_int2bv(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_bv_not); MATCH_UNARY(is_redand); MATCH_UNARY(is_redor); @@ -439,6 +440,7 @@ public: MATCH_BINARY(is_bv_smod0); MATCH_UNARY(is_bit2bool); MATCH_UNARY(is_int2bv); + END_DISABLE_WARNING; bool is_bit2bool(expr* e, expr*& bv, unsigned& idx) const; rational norm(rational const & val, unsigned bv_size, bool is_signed = false) const ; diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index 686b7105fe..0501c78b59 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -22,6 +22,7 @@ Revision History: --*/ #pragma once +#include "util/manage_warnings.h" #include "util/zstring.h" #include "ast/ast.h" #include @@ -97,11 +98,13 @@ public: bool is_bv2char(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_FROM_BV); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_is_digit); MATCH_UNARY(is_to_int); MATCH_UNARY(is_char2bv); MATCH_UNARY(is_bv2char); MATCH_BINARY(is_le); + END_DISABLE_WARNING; static unsigned max_char() { return zstring::max_char(); } diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index f7d65f2b43..ba26a05ef6 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -27,6 +27,7 @@ Revision History: #include "util/symbol_table.h" #include "util/obj_hashtable.h" #include "util/dictionary.h" +#include "util/manage_warnings.h" enum sort_kind { @@ -424,9 +425,13 @@ namespace datatype { bool is_recognizer(expr const * f) const { return is_app(f) && (is_recognizer0(to_app(f)) || is_is(to_app(f))); } bool is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args); + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_recognizer); + END_DISABLE_WARNING; bool is_accessor(expr const* e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_accessor); + END_DISABLE_WARNING; bool is_update_field(expr * f) const { return is_app(f) && is_app_of(to_app(f), fid(), OP_DT_UPDATE_FIELD); } app* mk_is(func_decl * c, expr *f); ptr_vector const * get_datatype_constructors(sort * ty); diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index ea9ab19f07..d73f8e71cb 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -30,6 +30,7 @@ Operators: #include "ast/ast.h" #include "ast/polymorphism_util.h" +#include "util/manage_warnings.h" enum finite_set_sort_kind { FINITE_SET_SORT @@ -137,6 +138,7 @@ public: bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); } bool is_unique_set(expr const *n) const { return is_app_of(n, m_fid, OP_FINITE_SET_UNIQUE_SET); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_singleton); MATCH_UNARY(is_size); MATCH_BINARY(is_union); @@ -148,6 +150,7 @@ public: MATCH_BINARY(is_filter); MATCH_BINARY(is_range); MATCH_BINARY(is_unique_set); + END_DISABLE_WARNING; }; class finite_set_util : public finite_set_recognizers { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 39b3fc33c4..a32d045ac8 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -22,6 +22,7 @@ Revision History: #include "util/id_gen.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "util/manage_warnings.h" #include "util/mpf.h" enum fpa_sort_kind { @@ -366,6 +367,8 @@ public: bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args); + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_TERNARY(is_fp); + END_DISABLE_WARNING; }; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index b9d885e018..798218bc0d 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -23,6 +23,7 @@ Notes: #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/th_rewriter.h" #include "util/ref_util.h" +#include "util/manage_warnings.h" #include "ast/ast_smt2_pp.h" struct blaster_cfg { @@ -246,9 +247,11 @@ void OP(expr * arg, expr_ref & result) { \ result = mk_mkbv(m_out); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_UNARY_REDUCE(reduce_not, mk_not); MK_UNARY_REDUCE(reduce_redor, mk_redor); MK_UNARY_REDUCE(reduce_redand, mk_redand); + END_DISABLE_WARNING; #define MK_BIN_REDUCE(OP, BB_OP) \ void OP(expr * arg1, expr * arg2, expr_ref & result) { \ @@ -260,6 +263,7 @@ void OP(expr * arg1, expr * arg2, expr_ref & result) { \ result = mk_mkbv(m_out); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_BIN_REDUCE(reduce_shl, mk_shl); MK_BIN_REDUCE(reduce_ashr, mk_ashr); MK_BIN_REDUCE(reduce_lshr, mk_lshr); @@ -270,6 +274,7 @@ void OP(expr * arg1, expr * arg2, expr_ref & result) { \ MK_BIN_REDUCE(reduce_smod, mk_smod); MK_BIN_REDUCE(reduce_ext_rotate_left, mk_ext_rotate_left); MK_BIN_REDUCE(reduce_ext_rotate_right, mk_ext_rotate_right); + END_DISABLE_WARNING; #define MK_BIN_AC_REDUCE(OP, BIN_OP, BB_OP) \ MK_BIN_REDUCE(BIN_OP, BB_OP); \ @@ -283,12 +288,14 @@ void OP(unsigned num_args, expr * const * args, expr_ref & result) { \ } \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder); MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier); MK_BIN_AC_REDUCE(reduce_and, reduce_bin_and, mk_and); MK_BIN_AC_REDUCE(reduce_or, reduce_bin_or, mk_or); MK_BIN_AC_REDUCE(reduce_xor, reduce_bin_xor, mk_xor); + END_DISABLE_WARNING; #define MK_BIN_PRED_REDUCE(OP, BB_OP) \ @@ -299,12 +306,14 @@ void OP(expr * arg1, expr * arg2, expr_ref & result) { m_blaster.BB_OP(m_in1.size(), m_in1.data(), m_in2.data(), result); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_BIN_PRED_REDUCE(reduce_eq, mk_eq); MK_BIN_PRED_REDUCE(reduce_sle, mk_sle); MK_BIN_PRED_REDUCE(reduce_ule, mk_ule); MK_BIN_PRED_REDUCE(reduce_umul_no_overflow, mk_umul_no_overflow); MK_BIN_PRED_REDUCE(reduce_smul_no_overflow, mk_smul_no_overflow); MK_BIN_PRED_REDUCE(reduce_smul_no_underflow, mk_smul_no_underflow); + END_DISABLE_WARNING; #define MK_PARAMETRIC_UNARY_REDUCE(OP, BB_OP) \ void OP(expr * arg, unsigned n, expr_ref & result) { \ @@ -315,7 +324,9 @@ void OP(expr * arg, unsigned n, expr_ref & result) { \ result = mk_mkbv(m_out); \ } +START_DISABLE_EXTRA_SEMI_WARNING; MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); +END_DISABLE_WARNING; void reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_in1.reset(); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 87785d8f82..04585c4c20 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -20,6 +20,7 @@ Revision History: #include "util/rational.h" #include "util/common_msgs.h" +#include "util/manage_warnings.h" #include "ast/rewriter/bit_blaster/bit_blaster_tpl.h" #include "ast/ast_pp.h" #include "ast/rewriter/rewriter_types.h" @@ -1075,12 +1076,14 @@ void bit_blaster_tpl::NAME(unsigned sz, expr * const * a_bits, expr * const } \ } +START_DISABLE_EXTRA_SEMI_WARNING; MK_BINARY(mk_and, mk_and); MK_BINARY(mk_or, mk_or); MK_BINARY(mk_xor, mk_xor); MK_BINARY(mk_xnor, mk_iff); MK_BINARY(mk_nand, mk_nand); MK_BINARY(mk_nor, mk_nor); +END_DISABLE_WARNING; template void bit_blaster_tpl::mk_redand(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits) { diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 713a0790bb..746b8b7b07 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -22,6 +22,7 @@ Notes: #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/mk_extract_proc.h" +#include "util/manage_warnings.h" class bv_rewriter_core { protected: @@ -237,12 +238,14 @@ public: return result; } + START_DISABLE_EXTRA_SEMI_WARNING; MK_BV_BINARY(mk_bv_urem); MK_BV_BINARY(mk_ule); MK_BV_BINARY(mk_sle); MK_BV_BINARY(mk_bv_add); MK_BV_BINARY(mk_bv_mul); MK_BV_BINARY(mk_bv_sub); + END_DISABLE_WARNING; expr_ref mk_ubv2int(expr* a) { diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 39cf2534fe..a3e5d2d9fc 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -21,6 +21,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" +#include "util/manage_warnings.h" namespace seq { @@ -147,7 +148,9 @@ namespace seq { bool is_align(expr const* e) const { return is_skolem(symbol("seq.align.m"), e); } bool is_align_l(expr const* e) const { return is_skolem(symbol("seq.align.l"), e); } bool is_align_r(expr const* e) const { return is_skolem(symbol("seq.align.r"), e); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_BINARY(is_align); + END_DISABLE_WARNING; bool is_post(expr* e, expr*& s, expr*& start); bool is_pre(expr* e, expr*& s, expr*& i); bool is_eq(expr* e, expr*& a, expr*& b) const; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index fd5696f493..bfe400c57e 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -25,6 +25,7 @@ Revision History: #include "ast/ast.h" #include "ast/char_decl_plugin.h" #include "util/lbool.h" +#include "util/manage_warnings.h" #include "util/zstring.h" enum seq_sort_kind { @@ -271,10 +272,12 @@ public: app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_BINARY(is_char_le); MATCH_UNARY(is_char2int); MATCH_UNARY(is_char2bv); MATCH_UNARY(is_bv2char); + END_DISABLE_WARNING; bool has_re() const { return seq.has_re(); } bool has_seq() const { return seq.has_seq(); } @@ -394,6 +397,7 @@ public: return (u.is_seq(s) && !u.is_string(s)); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_BINARY(is_concat); MATCH_UNARY(is_length); MATCH_TERNARY(is_extract); @@ -425,6 +429,7 @@ public: MATCH_UNARY(is_to_code); MATCH_BINARY(is_in_re); MATCH_UNARY(is_unit); + END_DISABLE_WARNING; void get_concat(expr* e, expr_ref_vector& es) const; void get_concat(expr* e, ptr_vector& es) const; @@ -579,6 +584,7 @@ public: bool is_of_pred(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OF_PRED); } bool is_reverse(expr const* n) const { return is_app_of(n, m_fid, OP_RE_REVERSE); } bool is_derivative(expr const* n) const { return is_app_of(n, m_fid, OP_RE_DERIVATIVE); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); MATCH_BINARY(is_union); @@ -593,6 +599,7 @@ public: MATCH_UNARY(is_of_pred); MATCH_UNARY(is_reverse); MATCH_BINARY(is_derivative); + END_DISABLE_WARNING; bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const; bool is_loop(expr const* n, expr*& body, unsigned& lo) const; bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index f1a8dee047..5af40497b4 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -23,6 +23,7 @@ Notes: #include "util/scoped_timer.h" #include "util/scoped_ctrl_c.h" #include "util/cancel_eh.h" +#include "util/manage_warnings.h" #include "model/model_smt2_pp.h" #include "ast/ast_smt2_pp.h" #include "tactic/tactic.h" @@ -733,6 +734,7 @@ static probe * NAME ## _probe (cmd_context & ctx, sexpr * n) { return NAME(p1.get(), p2.get()); \ } +START_DISABLE_EXTRA_SEMI_WARNING; MK_BIN_PROBE(mk_eq); MK_BIN_PROBE(mk_le); MK_BIN_PROBE(mk_lt); @@ -741,6 +743,7 @@ MK_BIN_PROBE(mk_gt); MK_BIN_PROBE(mk_implies); MK_BIN_PROBE(mk_div); MK_BIN_PROBE(mk_sub); +END_DISABLE_WARNING; #define MK_NARY_PROBE(NAME) \ static probe * NAME ## _probe(cmd_context & ctx, sexpr * n) { \ @@ -762,10 +765,12 @@ static probe * NAME ## _probe(cmd_context & ctx, sexpr * n) { } \ } +START_DISABLE_EXTRA_SEMI_WARNING; MK_NARY_PROBE(mk_and); MK_NARY_PROBE(mk_or); MK_NARY_PROBE(mk_add); MK_NARY_PROBE(mk_mul); +END_DISABLE_WARNING; probe * sexpr2probe(cmd_context & ctx, sexpr * n) { if (n->is_symbol()) { diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 37c0559728..78e40fbe89 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -19,6 +19,7 @@ Notes: #pragma once #include "util/rational.h" +#include "util/manage_warnings.h" #include "util/mpq.h" #include "math/polynomial/polynomial.h" #include "util/z3_exception.h" @@ -431,12 +432,14 @@ AN_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, int) \ AN_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpz) \ AN_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpq) +START_DISABLE_EXTRA_SEMI_WARNING; AN_MK_COMPARISON(operator==, eq); AN_MK_COMPARISON(operator!=, neq); AN_MK_COMPARISON(operator<, lt); AN_MK_COMPARISON(operator<=, le); AN_MK_COMPARISON(operator>, gt); AN_MK_COMPARISON(operator>=, ge); +END_DISABLE_WARNING; #undef AN_MK_COMPARISON #undef AN_MK_COMPARISON_CORE diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index b256ffd15b..4ba57edf9f 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -28,6 +28,7 @@ Notes: #include "math/interval/interval.h" #include "util/z3_exception.h" #include "util/rlimit.h" +#include "util/manage_warnings.h" namespace realclosure { class num; @@ -339,12 +340,14 @@ RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, int) \ RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpz) \ RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpq) +START_DISABLE_EXTRA_SEMI_WARNING; RCF_MK_COMPARISON(operator==, eq); RCF_MK_COMPARISON(operator!=, neq); RCF_MK_COMPARISON(operator<, lt); RCF_MK_COMPARISON(operator<=, le); RCF_MK_COMPARISON(operator>, gt); RCF_MK_COMPARISON(operator>=, ge); +END_DISABLE_WARNING; #undef RCF_MK_COMPARISON #undef RCF_MK_COMPARISON_CORE @@ -364,10 +367,12 @@ RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, int) \ RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, mpz) \ RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, mpq) -RCF_MK_BINARY(operator+, add) -RCF_MK_BINARY(operator-, sub) -RCF_MK_BINARY(operator*, mul) -RCF_MK_BINARY(operator/, div) +START_DISABLE_EXTRA_SEMI_WARNING; +RCF_MK_BINARY(operator+, add); +RCF_MK_BINARY(operator-, sub); +RCF_MK_BINARY(operator*, mul); +RCF_MK_BINARY(operator/, div); +END_DISABLE_WARNING; #undef RCF_MK_BINARY #undef RCF_MK_BINARY_CORE diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 83d5fd28e1..b4bbeb3ba8 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "smt/smt_model_generator.h" #include "util/stats.h" +#include "util/manage_warnings.h" #define ENABLE_QUOT_REM_ENCODING 0 @@ -819,6 +820,7 @@ namespace smt { init_bits(e, bits); } + START_DISABLE_EXTRA_SEMI_WARNING; MK_UNARY(internalize_neg, mk_neg); MK_UNARY(internalize_not, mk_not); MK_UNARY(internalize_redand, mk_redand); @@ -843,6 +845,7 @@ namespace smt { MK_AC_BINARY(internalize_nor, mk_nor); MK_AC_BINARY(internalize_xnor, mk_xnor); MK_BINARY(internalize_comp, mk_comp); + END_DISABLE_WARNING; #define MK_PARAMETRIC_UNARY(NAME, BLAST_OP) \ void theory_bv::NAME(app * n) { \ @@ -857,10 +860,12 @@ namespace smt { init_bits(e, bits); \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_PARAMETRIC_UNARY(internalize_sign_extend, mk_sign_extend); MK_PARAMETRIC_UNARY(internalize_zero_extend, mk_zero_extend); MK_PARAMETRIC_UNARY(internalize_rotate_left, mk_rotate_left); MK_PARAMETRIC_UNARY(internalize_rotate_right, mk_rotate_right); + END_DISABLE_WARNING; void theory_bv::internalize_concat(app * n) { process_args(n); @@ -1006,9 +1011,11 @@ namespace smt { } \ } + START_DISABLE_EXTRA_SEMI_WARNING; MK_NO_OVFL(internalize_umul_no_overflow, mk_umul_no_overflow); MK_NO_OVFL(internalize_smul_no_overflow, mk_smul_no_overflow); MK_NO_OVFL(internalize_smul_no_underflow, mk_smul_no_underflow); + END_DISABLE_WARNING; template void theory_bv::internalize_le(app * n) { diff --git a/src/tactic/arith/bv2real_rewriter.h b/src/tactic/arith/bv2real_rewriter.h index 9e10d6de5b..b70bc2d4bb 100644 --- a/src/tactic/arith/bv2real_rewriter.h +++ b/src/tactic/arith/bv2real_rewriter.h @@ -22,6 +22,7 @@ Notes: #include "ast/rewriter/rewriter.h" #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "util/manage_warnings.h" // // bv2real[d,r](n,m) has interpretation: @@ -100,8 +101,10 @@ public: bool is_pos_lef(func_decl* f) const { return f == m_pos_le; } bool is_pos_lt(expr const* e) const { return is_app(e) && is_pos_ltf(to_app(e)->get_decl()); } bool is_pos_le(expr const* e) const { return is_app(e) && is_pos_lef(to_app(e)->get_decl()); } + START_DISABLE_EXTRA_SEMI_WARNING; MATCH_BINARY(is_pos_lt); MATCH_BINARY(is_pos_le); + END_DISABLE_WARNING; expr* mk_pos_lt(expr* s, expr* t) { return m().mk_app(m_pos_lt, s, t); } expr* mk_pos_le(expr* s, expr* t) { return m().mk_app(m_pos_le, s, t); } diff --git a/src/util/manage_warnings.h b/src/util/manage_warnings.h index adc6059646..8be99dc4cb 100644 --- a/src/util/manage_warnings.h +++ b/src/util/manage_warnings.h @@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation Module Name: - build_warnings.h + manage_warnings.h Abstract: diff --git a/src/util/mpbq.h b/src/util/mpbq.h index 1bb6c396ed..4d2aea04e6 100644 --- a/src/util/mpbq.h +++ b/src/util/mpbq.h @@ -26,6 +26,7 @@ Revision History: --*/ #pragma once +#include "util/manage_warnings.h" #include "util/mpq.h" #include "util/rational.h" #include "util/vector.h" @@ -328,12 +329,14 @@ inline bool EXTERNAL(scoped_mpbq const & a, TYPE const & b) { \ MPBQ_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, int) \ MPBQ_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpz) \ +START_DISABLE_EXTRA_SEMI_WARNING; MPBQ_MK_COMPARISON(operator==, eq); MPBQ_MK_COMPARISON(operator!=, neq); MPBQ_MK_COMPARISON(operator<, lt); MPBQ_MK_COMPARISON(operator<=, le); MPBQ_MK_COMPARISON(operator>, gt); MPBQ_MK_COMPARISON(operator>=, ge); +END_DISABLE_WARNING; #undef MPBQ_MK_COMPARISON #undef MPBQ_MK_COMPARISON_CORE