From 373b691709790b276e9b69c8c9c57ca1540c51fd Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 10:26:38 +0700 Subject: [PATCH] Use 'override' where possible. --- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_generalizers.h | 8 +- src/muz/transforms/dl_mk_synchronize.h | 2 +- src/opt/maxres.cpp | 10 +- src/opt/opt_cmds.cpp | 54 +++++------ src/opt/sortmax.cpp | 4 +- src/opt/wmax.cpp | 4 +- src/sat/ba_solver.h | 106 ++++++++++----------- src/sat/sat_lookahead.cpp | 2 +- src/sat/tactic/goal2sat.h | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_pb.cpp | 6 +- src/smt/theory_str.cpp | 2 +- src/solver/parallel_tactic.cpp | 12 +-- src/tactic/core/symmetry_reduce_tactic.cpp | 2 +- src/tactic/dependency_converter.cpp | 18 ++-- src/tactic/generic_model_converter.h | 2 +- src/tactic/tactical.cpp | 6 +- src/util/lp/lar_solver.h | 2 +- 19 files changed, 123 insertions(+), 123 deletions(-) diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index b0fb6c2d3..6f9758337 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -50,7 +50,7 @@ namespace{ contains_array_op_proc(ast_manager &manager) : m(manager), m_array_fid(m.mk_family_id("array")) {} - virtual bool operator()(expr *e) { + bool operator()(expr *e) override { return is_app(e) && to_app(e)->get_family_id() == m_array_fid; } }; diff --git a/src/muz/spacer/spacer_generalizers.h b/src/muz/spacer/spacer_generalizers.h index 45ae472bd..e83cc1bc9 100644 --- a/src/muz/spacer/spacer_generalizers.h +++ b/src/muz/spacer/spacer_generalizers.h @@ -117,11 +117,11 @@ class lemma_quantifier_generalizer : public lemma_generalizer { int m_offset; public: lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true); - virtual ~lemma_quantifier_generalizer() {} - virtual void operator()(lemma_ref &lemma); + ~lemma_quantifier_generalizer() override {} + void operator()(lemma_ref &lemma) override; - virtual void collect_statistics(statistics& st) const; - virtual void reset_statistics() {m_st.reset();} + void collect_statistics(statistics& st) const override; + void reset_statistics() override {m_st.reset();} private: bool generalize(lemma_ref &lemma, app *term); diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 6f4b3ca40..77f45e91f 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -126,7 +126,7 @@ namespace datalog { */ mk_synchronize(context & ctx, unsigned priority = 22500); - rule_set * operator()(rule_set const & source); + rule_set * operator()(rule_set const & source) override; }; }; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index f52c56a60..0b5f20db8 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -144,7 +144,7 @@ public: } } - virtual ~maxres() {} + ~maxres() override {} bool is_literal(expr* l) { return @@ -332,7 +332,7 @@ public: } - virtual lbool operator()() { + lbool operator()() override { m_defs.reset(); switch(m_st) { case s_primal: @@ -343,7 +343,7 @@ public: return l_undef; } - virtual void collect_statistics(statistics& st) const { + void collect_statistics(statistics& st) const override { st.update("maxres-cores", m_stats.m_num_cores); st.update("maxres-correction-sets", m_stats.m_num_cs); } @@ -781,7 +781,7 @@ public: TRACE("opt", tout << "after remove: " << asms << "\n";); } - virtual void updt_params(params_ref& _p) { + void updt_params(params_ref& _p) override { maxsmt_solver_base::updt_params(_p); opt_params p(_p); m_hill_climb = p.maxres_hill_climb(); @@ -816,7 +816,7 @@ public: return l_true; } - virtual void commit_assignment() { + void commit_assignment() override { if (m_found_feasible_optimum) { TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;); s().assert_expr(m_defs); diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index d8e301e08..f01df0bdd 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -56,33 +56,33 @@ public: m_opt(opt) {} - virtual ~assert_soft_cmd() { + ~assert_soft_cmd() override { } - virtual void reset(cmd_context & ctx) { + void reset(cmd_context & ctx) override { m_idx = 0; m_formula = nullptr; } - virtual char const * get_usage() const { return " [:weight ] [:id ]"; } - virtual char const * get_main_descr() const { return "assert soft constraint with optional weight and identifier"; } + char const * get_usage() const override { return " [:weight ] [:id ]"; } + char const * get_main_descr() const override { return "assert soft constraint with optional weight and identifier"; } // command invocation - virtual void prepare(cmd_context & ctx) { + void prepare(cmd_context & ctx) override { reset(ctx); } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { if (m_idx == 0) return CPK_EXPR; return parametric_cmd::next_arg_kind(ctx); } - virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { + void init_pdescrs(cmd_context & ctx, param_descrs & p) override { p.insert("weight", CPK_NUMERAL, "(default: 1) penalty of not satisfying constraint."); p.insert("id", CPK_SYMBOL, "(default: null) partition identifier for soft constraints."); } - virtual void set_next_arg(cmd_context & ctx, expr * t) { + void set_next_arg(cmd_context & ctx, expr * t) override { SASSERT(m_idx == 0); if (!ctx.m().is_bool(t)) { throw cmd_exception("Invalid type for expression. Expected Boolean type."); @@ -91,11 +91,11 @@ public: ++m_idx; } - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { if (!m_formula) { throw cmd_exception("assert-soft requires a formulas as argument."); } @@ -107,7 +107,7 @@ public: reset(ctx); } - virtual void finalize(cmd_context & ctx) { + void finalize(cmd_context & ctx) override { } }; @@ -123,14 +123,14 @@ public: m_opt(opt) {} - virtual void reset(cmd_context & ctx) { } - virtual char const * get_usage() const { return ""; } - virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";} - virtual unsigned get_arity() const { return 1; } - virtual void prepare(cmd_context & ctx) {} - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; } + void reset(cmd_context & ctx) override { } + char const * get_usage() const override { return ""; } + char const * get_descr(cmd_context & ctx) const override { return "check sat modulo objective function";} + unsigned get_arity() const override { return 1; } + void prepare(cmd_context & ctx) override {} + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; } - virtual void set_next_arg(cmd_context & ctx, expr * t) { + void set_next_arg(cmd_context & ctx, expr * t) override { if (!is_app(t)) { throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } @@ -138,11 +138,11 @@ public: ctx.print_success(); } - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { } }; @@ -154,18 +154,18 @@ public: m_opt(opt) {} - virtual void reset(cmd_context & ctx) { } - virtual char const * get_usage() const { return "(get-objectives)"; } - virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; } - virtual unsigned get_arity() const { return 0; } - virtual void prepare(cmd_context & ctx) {} + void reset(cmd_context & ctx) override { } + char const * get_usage() const override { return "(get-objectives)"; } + char const * get_descr(cmd_context & ctx) const override { return "retrieve the objective values (after optimization)"; } + unsigned get_arity() const override { return 0; } + void prepare(cmd_context & ctx) override {} - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { if (!ctx.ignore_check()) { get_opt(ctx, m_opt).display_assignment(ctx.regular_stream()); } diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 1fafa12bd..df361f24a 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -39,9 +39,9 @@ namespace opt { sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {} - virtual ~sortmax() {} + ~sortmax() override {} - lbool operator()() { + lbool operator()() override { obj_map soft; if (!init()) { return l_false; diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index e4eb7e06b..ee7f92a23 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -49,9 +49,9 @@ namespace opt { m_trail(m), m_defs(m) {} - virtual ~wmax() {} + ~wmax() override {} - lbool operator()() { + lbool operator()() override { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); obj_map soft; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index bae59f45a..26887e3b1 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -128,7 +128,7 @@ namespace sat { virtual void set_k(unsigned k) { VERIFY(k < 4000000000); m_k = k; } virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; } unsigned k() const { return m_k; } - virtual bool well_formed() const; + bool well_formed() const override; }; class card : public pb_base { @@ -140,13 +140,13 @@ namespace sat { literal& operator[](unsigned i) { return m_lits[i]; } literal const* begin() const { return m_lits; } literal const* end() const { return static_cast(m_lits) + m_size; } - virtual void negate(); - virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } - virtual literal_vector literals() const { return literal_vector(m_size, m_lits); } - virtual bool is_watching(literal l) const; - virtual literal get_lit(unsigned i) const { return m_lits[i]; } - virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; } - virtual unsigned get_coeff(unsigned i) const { return 1; } + void negate() override; + void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); } + literal_vector literals() const override { return literal_vector(m_size, m_lits); } + bool is_watching(literal l) const override; + literal get_lit(unsigned i) const override { return m_lits[i]; } + void set_lit(unsigned i, literal l) override { m_lits[i] = l; } + unsigned get_coeff(unsigned i) const override { return 1; } }; @@ -173,14 +173,14 @@ namespace sat { void update_max_sum(); void set_num_watch(unsigned s) { m_num_watch = s; } bool is_cardinality() const; - virtual void negate(); - virtual void set_k(unsigned k) { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } - virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); } - virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } - virtual bool is_watching(literal l) const; - virtual literal get_lit(unsigned i) const { return m_wlits[i].second; } - virtual void set_lit(unsigned i, literal l) { m_wlits[i].second = l; } - virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; } + void negate() override; + void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } + void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); } + literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } + bool is_watching(literal l) const override; + literal get_lit(unsigned i) const override { return m_wlits[i].second; } + void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; } + unsigned get_coeff(unsigned i) const override { return m_wlits[i].first; } }; class xr : public constraint { @@ -191,13 +191,13 @@ namespace sat { literal operator[](unsigned i) const { return m_lits[i]; } literal const* begin() const { return m_lits; } literal const* end() const { return begin() + m_size; } - virtual void negate() { m_lits[0].neg(); } - virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } - virtual bool is_watching(literal l) const; - virtual literal_vector literals() const { return literal_vector(size(), begin()); } - virtual literal get_lit(unsigned i) const { return m_lits[i]; } - virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; } - virtual bool well_formed() const; + void negate() override { m_lits[0].neg(); } + void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); } + bool is_watching(literal l) const override; + literal_vector literals() const override { return literal_vector(size(), begin()); } + literal get_lit(unsigned i) const override { return m_lits[i]; } + void set_lit(unsigned i, literal l) override { m_lits[i] = l; } + bool well_formed() const override; }; @@ -484,44 +484,44 @@ namespace sat { public: ba_solver(); - virtual ~ba_solver(); - virtual void set_solver(solver* s) { m_solver = s; } - virtual void set_lookahead(lookahead* l) { m_lookahead = l; } - virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; } + ~ba_solver() override; + void set_solver(solver* s) override { m_solver = s; } + void set_lookahead(lookahead* l) override { m_lookahead = l; } + void set_unit_walk(unit_walk* u) override { m_unit_walk = u; } void add_at_least(bool_var v, literal_vector const& lits, unsigned k); void add_pb_ge(bool_var v, svector const& wlits, unsigned k); void add_xr(literal_vector const& lits); - virtual bool propagate(literal l, ext_constraint_idx idx); - virtual lbool resolve_conflict(); - virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r); - virtual void asserted(literal l); - virtual check_result check(); - virtual void push(); - virtual void pop(unsigned n); - virtual void simplify(); - virtual void clauses_modifed(); - virtual lbool get_phase(bool_var v); - virtual bool set_root(literal l, literal r); - virtual void flush_roots(); - virtual std::ostream& display(std::ostream& out) const; - virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const; - virtual void collect_statistics(statistics& st) const; - virtual extension* copy(solver* s); - virtual extension* copy(lookahead* s, bool learned); - virtual void find_mutexes(literal_vector& lits, vector & mutexes); - virtual void pop_reinit(); - virtual void gc(); - virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const; - virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r); - virtual void init_use_list(ext_use_list& ul); - virtual bool is_blocked(literal l, ext_constraint_idx idx); - virtual bool check_model(model const& m) const; + bool propagate(literal l, ext_constraint_idx idx) override; + lbool resolve_conflict() override; + void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override; + void asserted(literal l) override; + check_result check() override; + void push() override; + void pop(unsigned n) override; + void simplify() override; + void clauses_modifed() override; + lbool get_phase(bool_var v) override; + bool set_root(literal l, literal r) override; + void flush_roots() override; + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; + void collect_statistics(statistics& st) const override; + extension* copy(solver* s) override; + extension* copy(lookahead* s, bool learned) override; + void find_mutexes(literal_vector& lits, vector & mutexes) override; + void pop_reinit() override; + void gc() override; + double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const override; + bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override; + void init_use_list(ext_use_list& ul) override; + bool is_blocked(literal l, ext_constraint_idx idx) override; + bool check_model(model const& m) const override; ptr_vector const & constraints() const { return m_constraints; } void display(std::ostream& out, constraint const& c, bool values) const; - virtual bool validate(); + bool validate() override; }; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index bbc1106bb..0da914b71 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1217,7 +1217,7 @@ namespace sat { lookahead& lh; public: lookahead_literal_occs_fun(lookahead& lh): lh(lh) {} - double operator()(literal l) { return lh.literal_occs(l); } + double operator()(literal l) override { return lh.literal_occs(l); } }; // Ternary clause managagement: diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index d86b2d7e4..514b65311 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -86,7 +86,7 @@ public: public: mc(ast_manager& m); - virtual ~mc() {} + ~mc() override {} // flush model converter from SAT solver to this structure. void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(model_ref& md) override; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index db031d043..a27f4ff83 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -147,7 +147,7 @@ class theory_lra::imp { imp& m_imp; public: resource_limit(imp& i): m_imp(i) { } - virtual bool get_cancel_flag() { return m_imp.m.canceled(); } + bool get_cancel_flag() override { return m_imp.m.canceled(); } }; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 2fb0187f8..90d1a5481 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -759,18 +759,18 @@ namespace smt { card& get_card() { return m_card; } - virtual void get_antecedents(conflict_resolution& cr) { + void get_antecedents(conflict_resolution& cr) override { cr.mark_literal(m_card.lit()); for (unsigned i = m_card.k(); i < m_card.size(); ++i) { cr.mark_literal(~m_card.lit(i)); } } - virtual theory_id get_from_theory() const { + theory_id get_from_theory() const override { return m_fid; } - virtual proof* mk_proof(smt::conflict_resolution& cr) { + proof* mk_proof(smt::conflict_resolution& cr) override { ptr_buffer prs; ast_manager& m = cr.get_context().get_manager(); expr_ref fact(m); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d902aa533..324e1f54a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -110,7 +110,7 @@ namespace smt { public: seq_expr_solver(ast_manager& m, smt_params& fp): m_kernel(m, fp) {} - virtual lbool check_sat(expr* e) { + lbool check_sat(expr* e) override { m_kernel.push(); m_kernel.assert_expr(e); lbool r = m_kernel.check(); diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index f0bb65315..4ee93ff37 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -672,7 +672,7 @@ public: init(); } - void operator ()(const goal_ref & g,goal_ref_buffer & result) { + void operator ()(const goal_ref & g,goal_ref_buffer & result) override { fail_if_proof_generation("parallel-tactic", g); ast_manager& m = g->m(); solver* s = m_solver->translate(m, m_params); @@ -719,29 +719,29 @@ public: return pp.conquer_batch_size(); } - void cleanup() { + void cleanup() override { m_queue.reset(); } - tactic* translate(ast_manager& m) { + tactic* translate(ast_manager& m) override { solver* s = m_solver->translate(m, m_params); return alloc(parallel_tactic, s, m_params); } - virtual void updt_params(params_ref const & p) { + void updt_params(params_ref const & p) override { m_params.copy(p); parallel_params pp(p); m_conquer_delay = pp.conquer_delay(); } - virtual void collect_statistics(statistics & st) const { + void collect_statistics(statistics & st) const override { st.copy(m_stats); st.update("par unsat", m_num_unsat); st.update("par models", m_models.size()); st.update("par progress", m_progress); } - virtual void reset_statistics() { + void reset_statistics() override { m_stats.reset(); } }; diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index d288adbc7..784686a5e 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -40,7 +40,7 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override; - virtual void cleanup() override; + void cleanup() override; }; class ac_rewriter { diff --git a/src/tactic/dependency_converter.cpp b/src/tactic/dependency_converter.cpp index 34c864526..dcd50717b 100644 --- a/src/tactic/dependency_converter.cpp +++ b/src/tactic/dependency_converter.cpp @@ -27,15 +27,15 @@ public: unit_dependency_converter(expr_dependency_ref& d) : m_dep(d) {} - virtual expr_dependency_ref operator()() { return m_dep; } + expr_dependency_ref operator()() override { return m_dep; } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { expr_dependency_translation tr(translator); expr_dependency_ref d(tr(m_dep), translator.to()); return alloc(unit_dependency_converter, d); } - virtual void display(std::ostream& out) { + void display(std::ostream& out) override { out << m_dep.get() << "\n"; } }; @@ -47,18 +47,18 @@ public: concat_dependency_converter(dependency_converter* c1, dependency_converter* c2) : m_dc1(c1), m_dc2(c2) {} - virtual expr_dependency_ref operator()() { + expr_dependency_ref operator()() override { expr_dependency_ref d1 = (*m_dc1)(); expr_dependency_ref d2 = (*m_dc2)(); ast_manager& m = d1.get_manager(); return expr_dependency_ref(m.mk_join(d1, d2), m); } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { return alloc(concat_dependency_converter, m_dc1->translate(translator), m_dc2->translate(translator)); } - virtual void display(std::ostream& out) { + void display(std::ostream& out) override { m_dc1->display(out); m_dc2->display(out); } @@ -73,7 +73,7 @@ public: for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]); } - virtual expr_dependency_ref operator()() { + expr_dependency_ref operator()() override { expr_dependency_ref result(m.mk_empty_dependencies(), m); for (goal_ref g : m_goals) { dependency_converter_ref dc = g->dc(); @@ -81,13 +81,13 @@ public: } return result; } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { goal_ref_buffer goals; for (goal_ref g : m_goals) goals.push_back(g->translate(translator)); return alloc(goal_dependency_converter, goals.size(), goals.c_ptr()); } - virtual void display(std::ostream& out) { out << "goal-dep\n"; } + void display(std::ostream& out) override { out << "goal-dep\n"; } }; diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 69bc35a3f..750a22cd4 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -41,7 +41,7 @@ class generic_model_converter : public model_converter { public: generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} - virtual ~generic_model_converter(); + ~generic_model_converter() override; void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index a71ea738c..98f6be343 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -744,7 +744,7 @@ public: SASSERT(t); } - virtual ~unary_tactical() { } + ~unary_tactical() override { } void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); @@ -1003,7 +1003,7 @@ public: SASSERT(m_p); } - virtual ~cond_tactical() {} + ~cond_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (m_p->operator()(*(in.get())).is_true()) @@ -1035,7 +1035,7 @@ public: SASSERT(m_p); } - virtual ~fail_if_tactic() {} + ~fail_if_tactic() override {} void cleanup() override {} diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 4189bad4e..8541a9b86 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -397,7 +397,7 @@ public: column_type get_column_type(unsigned j) const; - std::string get_column_name(unsigned j) const; + std::string get_column_name(unsigned j) const override; bool all_constrained_variables_are_registered(const vector>& left_side);