From 7ce5b687fab4de66f2d6c213df0ffefe4282ada5 Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Wed, 17 Jun 2026 08:29:36 -0700 Subject: [PATCH] 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)