From 1eb84fe4b991c492a58ddbecefc2758f1c196771 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 30 Jul 2022 04:29:15 +0700 Subject: [PATCH] Mark override methods appropriately. (#6207) --- src/api/api_algebraic.cpp | 2 +- src/api/api_context.h | 2 +- src/ast/fpa/fpa2bv_converter.h | 2 +- src/ast/rewriter/push_app_ite.h | 2 +- src/ast/value_generator.cpp | 2 +- src/math/lp/factorization_factory_imp.h | 6 +++--- src/math/lp/lar_solver.h | 4 ++-- src/math/lp/lp_solver.h | 2 +- src/math/subpaving/tactic/subpaving_tactic.cpp | 2 +- src/nlsat/nlsat_assignment.h | 2 +- src/sat/smt/sat_th.h | 2 +- src/smt/smt_model_finder.cpp | 2 +- src/tactic/tactic.h | 2 +- src/test/dl_product_relation.cpp | 2 +- src/util/trail.h | 2 +- 15 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index d24a4a624..969de515c 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -344,7 +344,7 @@ extern "C" { scoped_anum_vector const & m_as; public: vector_var2anum(scoped_anum_vector & as):m_as(as) {} - virtual ~vector_var2anum() {} + ~vector_var2anum() override {} algebraic_numbers::manager & m() const override { return m_as.m(); } bool contains(polynomial::var x) const override { return static_cast(x) < m_as.size(); } algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 182958b1e..3bc0d4403 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,7 +58,7 @@ namespace api { solver_ref s; public: seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {} - lbool check_sat(expr* e) { + lbool check_sat(expr* e) override { if (!s) { s = mk_smt_solver(m, p, symbol("ALL")); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index d663fda95..a5bdce3df 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -239,7 +239,7 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter { fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) : fpa2bv_converter(m), m_rw(rw) {} - virtual ~fpa2bv_converter_wrapped() {} + ~fpa2bv_converter_wrapped() override {} void mk_const(func_decl * f, expr_ref & result) override; void mk_rm_const(func_decl * f, expr_ref & result) override; app_ref wrap(expr * e); diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h index a2e18dd25..e30feac1c 100644 --- a/src/ast/rewriter/push_app_ite.h +++ b/src/ast/rewriter/push_app_ite.h @@ -49,7 +49,7 @@ protected: bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override; public: ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {} - virtual ~ng_push_app_ite_cfg() {} + ~ng_push_app_ite_cfg() override {} }; struct push_app_ite_rw : public rewriter_tpl { diff --git a/src/ast/value_generator.cpp b/src/ast/value_generator.cpp index ef21f2444..6e52afba3 100644 --- a/src/ast/value_generator.cpp +++ b/src/ast/value_generator.cpp @@ -99,7 +99,7 @@ public: datatype_value_generator(value_generator& g, ast_manager& m): m(m), g(g), dt(m), m_sorts(m) {} - ~datatype_value_generator() { + ~datatype_value_generator() override { for (auto& kv : m_values) dealloc(kv.m_value); } diff --git a/src/math/lp/factorization_factory_imp.h b/src/math/lp/factorization_factory_imp.h index b404d5f14..599039094 100644 --- a/src/math/lp/factorization_factory_imp.h +++ b/src/math/lp/factorization_factory_imp.h @@ -28,8 +28,8 @@ namespace nla { const monic& m_rm; factorization_factory_imp(const monic& rm, const core& s); - bool find_canonical_monic_of_vars(const svector& vars, unsigned & i) const; - virtual bool canonize_sign(const monic& m) const; - virtual bool canonize_sign(const factorization& m) const; + bool find_canonical_monic_of_vars(const svector& vars, unsigned & i) const override; + bool canonize_sign(const monic& m) const override; + bool canonize_sign(const factorization& m) const override; }; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index f1cbd3370..cce63855d 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -543,7 +543,7 @@ public: void get_model(std::unordered_map & variable_values) const; void get_rid_of_inf_eps(); void get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const; - std::string get_variable_name(var_index vi) const; + std::string get_variable_name(var_index vi) const override; void set_variable_name(var_index vi, std::string); inline unsigned number_of_vars() const { return m_var_register.size(); } inline bool is_base(unsigned j) const { return m_mpq_lar_core_solver.m_r_heading[j] >= 0; } @@ -651,7 +651,7 @@ public: lar_solver(); void set_track_pivoted_rows(bool v); bool get_track_pivoted_rows() const; - virtual ~lar_solver(); + ~lar_solver() override; const vector& r_x() const { return m_mpq_lar_core_solver.m_r_x; } bool column_is_int(unsigned j) const; inline bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h index 68beca06f..ab16a686f 100644 --- a/src/math/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -149,7 +149,7 @@ public: } - virtual ~lp_solver(); + ~lp_solver() override; void flip_costs(); diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index cdd8bac0a..4aa8f6ccd 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -37,7 +37,7 @@ class subpaving_tactic : public tactic { e2v.mk_inv(m_inv); } - virtual ~display_var_proc() {} + ~display_var_proc() override {} ast_manager & m() const { return m_inv.get_manager(); } diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h index 11e82fd30..3f4c3b95a 100644 --- a/src/nlsat/nlsat_assignment.h +++ b/src/nlsat/nlsat_assignment.h @@ -32,7 +32,7 @@ namespace nlsat { bool_vector m_assigned; public: assignment(anum_manager & _m):m_values(_m) {} - virtual ~assignment() {} + ~assignment() override {} anum_manager & am() const { return m_values.m(); } void swap(assignment & other) { m_values.swap(other.m_values); diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 4484a7717..430b1c431 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -189,7 +189,7 @@ namespace euf { public: th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id); - virtual ~th_euf_solver() {} + ~th_euf_solver() override {} virtual theory_var mk_var(enode* n); unsigned get_num_vars() const { return m_var2enode.size(); } euf::enode* e_internalize(expr* e); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 34f323695..35b350e79 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -464,7 +464,7 @@ namespace smt { m.limit().inc(); } - virtual ~auf_solver() { + ~auf_solver() override { flush_nodes(); reset_eval_cache(); } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index af8b24b2f..bc87cdf18 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -35,7 +35,7 @@ class tactic : public user_propagator::core { unsigned m_ref_count; public: tactic():m_ref_count(0) {} - virtual ~tactic() {} + ~tactic() override {} void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index 5b5c196d5..9d841e421 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -22,7 +22,7 @@ namespace datalog { public: collector_of_reduced(idx_set & accumulator) : m_acc(accumulator) {} - virtual void operator()(table_element * func_columns, const table_element * merged_func_columns) { + void operator()(table_element * func_columns, const table_element * merged_func_columns) override { m_acc.insert(static_cast(merged_func_columns[0])); } }; diff --git a/src/util/trail.h b/src/util/trail.h index 969c4a746..9a7ec4303 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -243,7 +243,7 @@ public: m_value(m_vector.back()) { } - virtual void undo() { + void undo() override { m_vector.push_back(m_value); } };