mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Fix "override"-related warnings.

Browse source
This commit is contained in:
David Detlefs 2026-06-17 08:29:36 -07:00
parent 3a470de4ff
commit 7ce5b687fa
4 changed files with 48 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

68
src/cmd_context/cmd_util.h
View file

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

2
src/math/lp/dioph_eq.cpp
View file

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

10
src/math/lp/static_matrix.h
View file

@ -119,9 +119,9 @@ public:
void init_empty_matrix(unsigned m, unsigned n);
unsigned row_count() const { return static_cast<unsigned>(m_rows.size()); }
unsigned row_count() const override { return static_cast<unsigned>(m_rows.size()); }
unsigned column_count() const { return static_cast<unsigned>(m_columns.size()); }
unsigned column_count() const override { return static_cast<unsigned>(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<unsigned>(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;

10
src/solver/assertions/asserted_formulas.h
View file

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