From 5014b1a34d3ebfe3b1963ee6580c4db7ef541cbd Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 4 Aug 2022 13:21:07 +0700 Subject: [PATCH] Use `= default` for virtual constructors. --- src/api/api_util.h | 2 +- src/api/c++/z3++.h | 2 +- src/ast/ast.h | 4 ++-- src/ast/ast_printer.h | 2 +- src/ast/ast_smt2_pp.h | 2 +- src/ast/datatype_decl_plugin.h | 2 +- src/ast/expr_functors.h | 4 ++-- src/ast/macros/quantifier_macro_info.h | 2 +- src/ast/normal_forms/elim_term_ite.h | 2 +- src/ast/normal_forms/name_exprs.h | 2 +- src/ast/recfun_decl_plugin.h | 2 +- src/ast/rewriter/expr_replacer.h | 2 +- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/substitution/substitution_tree.h | 2 +- src/ast/value_generator.h | 2 +- src/cmd_context/cmd_context.h | 2 +- src/cmd_context/pdecl.cpp | 2 +- src/cmd_context/pdecl.h | 4 ++-- src/math/automata/boolean_algebra.h | 2 +- src/math/hilbert/heap_trie.h | 2 +- src/math/lp/lar_constraints.h | 2 +- src/math/lp/lp_api.h | 2 +- src/math/lp/matrix.h | 2 +- src/math/lp/nex.h | 2 +- src/math/lp/tail_matrix.h | 2 +- src/math/simplex/network_flow.h | 2 +- src/math/subpaving/subpaving.h | 2 +- src/math/subpaving/subpaving_t.h | 6 +++--- src/model/model_macro_solver.h | 4 ++-- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_engine_base.h | 2 +- src/muz/base/dl_rule_transformer.h | 2 +- src/muz/fp/datalog_parser.h | 4 ++-- src/muz/rel/dl_base.h | 16 ++++++++-------- src/muz/rel/dl_external_relation.h | 2 +- src/muz/rel/dl_instruction.h | 2 +- src/muz/rel/dl_lazy_table.h | 2 +- src/muz/rel/dl_relation_manager.cpp | 4 ++-- src/muz/rel/dl_sparse_table.cpp | 2 +- src/muz/rel/dl_table_plugin.h | 4 ++-- src/muz/spacer/spacer_context.h | 2 +- src/muz/spacer/spacer_unsat_core_plugin.h | 2 +- src/opt/maxsmt.h | 2 +- src/opt/opt_lns.h | 2 +- src/opt/opt_pareto.h | 2 +- src/opt/opt_sls_solver.h | 2 +- src/qe/mbp/mbp_plugin.h | 2 +- src/qe/mbp/mbp_solve_plugin.h | 2 +- src/qe/nlarith_util.h | 4 ++-- src/qe/qe.cpp | 2 +- src/qe/qe.h | 2 +- src/qe/qe_mbi.h | 2 +- src/sat/sat_extension.h | 2 +- src/sat/sat_solver_core.h | 2 +- src/sat/sat_types.h | 2 +- src/sat/smt/q_mam.h | 2 +- src/sat/smt/q_model_fixer.h | 2 +- src/sat/smt/sat_internalizer.h | 2 +- src/sat/smt/sat_th.h | 6 +++--- src/smt/mam.h | 3 +-- src/smt/smt_case_split_queue.h | 2 +- src/smt/smt_clause.h | 2 +- src/smt/smt_for_each_relevant_expr.h | 2 +- src/smt/smt_justification.h | 2 +- src/smt/smt_model_finder.cpp | 2 +- src/smt/smt_model_generator.h | 2 +- src/smt/smt_quantifier.h | 2 +- src/smt/smt_relevancy.h | 4 ++-- src/smt/theory_arith.h | 2 +- src/smt/theory_bv.h | 2 +- src/smt/theory_seq.h | 2 +- src/solver/check_sat_result.h | 2 +- src/solver/progress_callback.h | 2 +- src/solver/solver.h | 4 ++-- src/tactic/bv/bv_bound_chk_tactic.cpp | 2 +- src/tactic/converter.h | 2 +- src/tactic/core/ctx_simplify_tactic.h | 2 +- src/tactic/core/dom_simplify_tactic.h | 2 +- src/tactic/probe.h | 2 +- src/tactic/user_propagator_base.h | 2 +- src/test/ex.cpp | 2 +- src/util/cmd_context_types.h | 2 +- src/util/event_handler.h | 2 +- src/util/trail.h | 2 +- src/util/z3_exception.h | 2 +- 85 files changed, 106 insertions(+), 107 deletions(-) diff --git a/src/api/api_util.h b/src/api/api_util.h index 80f4f5ec705..0ff2c8dddef 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -40,7 +40,7 @@ namespace api { context& m_context; public: object(context& c); - virtual ~object() {} + virtual ~object() = default; unsigned ref_count() const { return m_ref_count; } unsigned id() const { return m_id; } void inc_ref(); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4012c00d478..8d3a70b8b5e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -87,7 +87,7 @@ namespace z3 { class exception : public std::exception { std::string m_msg; public: - virtual ~exception() throw() {} + virtual ~exception() throw() = default; exception(char const * msg):m_msg(msg) {} char const * msg() const { return m_msg.c_str(); } char const * what() const throw() { return m_msg.c_str(); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 798280d2c2b..d8eb072e374 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1024,7 +1024,7 @@ class decl_plugin { friend class ast_manager; public: - virtual ~decl_plugin() {} + virtual ~decl_plugin() = default; virtual void finalize() {} @@ -2582,7 +2582,7 @@ class ast_mark { obj_mark m_expr_marks; obj_mark m_decl_marks; public: - virtual ~ast_mark() {} + virtual ~ast_mark() = default; bool is_marked(ast * n) const; virtual void mark(ast * n, bool flag); virtual void reset(); diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h index 37023393f32..bea01e82697 100644 --- a/src/ast/ast_printer.h +++ b/src/ast/ast_printer.h @@ -24,7 +24,7 @@ Revision History: class ast_printer { public: - virtual ~ast_printer() {} + virtual ~ast_printer() = default; virtual void pp(sort * s, format_ns::format_ref & r) const { UNREACHABLE(); } virtual void pp(func_decl * f, format_ns::format_ref & r) const { UNREACHABLE(); } virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const { UNREACHABLE(); } diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index dbf9340ad73..47649b9b265 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -46,7 +46,7 @@ class smt2_pp_environment { format_ns::format * pp_as(format_ns::format * fname, sort * s); format_ns::format * pp_signature(format_ns::format * f_name, func_decl * f); public: - virtual ~smt2_pp_environment() {} + virtual ~smt2_pp_environment() = default; virtual ast_manager & get_manager() const = 0; virtual arith_util & get_autil() = 0; virtual bv_util & get_bvutil() = 0; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 0698bf821a9..31017578155 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -105,7 +105,7 @@ namespace datatype { class size { unsigned m_ref{ 0 }; public: - virtual ~size() { } + virtual ~size() = default; void inc_ref() { ++m_ref; } void dec_ref(); static size* mk_offset(sort_size const& s); diff --git a/src/ast/expr_functors.h b/src/ast/expr_functors.h index 4e87fb39eed..af669f48e72 100644 --- a/src/ast/expr_functors.h +++ b/src/ast/expr_functors.h @@ -27,14 +27,14 @@ Revision History: class i_expr_pred { public: virtual bool operator()(expr* e) = 0; - virtual ~i_expr_pred() {} + virtual ~i_expr_pred() = default; }; class i_sort_pred { public: virtual bool operator()(sort* s) = 0; - virtual ~i_sort_pred() {} + virtual ~i_sort_pred() = default; }; diff --git a/src/ast/macros/quantifier_macro_info.h b/src/ast/macros/quantifier_macro_info.h index 82790e937c2..646b31c88c4 100644 --- a/src/ast/macros/quantifier_macro_info.h +++ b/src/ast/macros/quantifier_macro_info.h @@ -39,7 +39,7 @@ class quantifier_macro_info { void collect_macro_candidates(quantifier* q); public: quantifier_macro_info(ast_manager& m, quantifier* q); - virtual ~quantifier_macro_info() {} + virtual ~quantifier_macro_info() = default; bool is_auf() const { return m_is_auf; } quantifier* get_flat_q() const { return m_flat_q; } bool has_cond_macros() const { return !m_cond_macros.empty(); } diff --git a/src/ast/normal_forms/elim_term_ite.h b/src/ast/normal_forms/elim_term_ite.h index 60f2ad8f7d7..36302ad1ea8 100644 --- a/src/ast/normal_forms/elim_term_ite.h +++ b/src/ast/normal_forms/elim_term_ite.h @@ -31,7 +31,7 @@ class elim_term_ite_cfg : public default_rewriter_cfg { elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) { // TBD enable_ac_support(false); } - virtual ~elim_term_ite_cfg() {} + virtual ~elim_term_ite_cfg() = default; vector const& new_defs() const { return m_new_defs; } br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr); void push() { m_lim.push_back(m_new_defs.size()); } diff --git a/src/ast/normal_forms/name_exprs.h b/src/ast/normal_forms/name_exprs.h index 268df88211f..4f652bce882 100644 --- a/src/ast/normal_forms/name_exprs.h +++ b/src/ast/normal_forms/name_exprs.h @@ -29,7 +29,7 @@ class expr_predicate { class name_exprs { public: - virtual ~name_exprs() {} + virtual ~name_exprs() = default; virtual void operator()(expr * n, // [IN] expression that contain the sub-expressions to be named expr_ref_vector & new_defs, // [OUT] new definitions proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index bbc4e5810a8..dcff35e82ee 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -49,7 +49,7 @@ namespace recfun { class replace { public: - virtual ~replace() {} + virtual ~replace() = default; virtual void reset() = 0; virtual void insert(expr* d, expr* r) = 0; virtual expr_ref operator()(expr* e) = 0; diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index e587faad751..82982adff4c 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -28,7 +28,7 @@ Module Name: class expr_replacer { struct scoped_set_subst; public: - virtual ~expr_replacer() {} + virtual ~expr_replacer() = default; virtual ast_manager & m() const = 0; virtual void set_substitution(expr_substitution * s) = 0; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 4c7c3883adc..cb00938d7f7 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -83,7 +83,7 @@ class sym_expr_manager { class expr_solver { public: - virtual ~expr_solver() {} + virtual ~expr_solver() = default; virtual lbool check_sat(expr* e) = 0; }; diff --git a/src/ast/substitution/substitution_tree.h b/src/ast/substitution/substitution_tree.h index c94bb4eea94..13993c171fb 100644 --- a/src/ast/substitution/substitution_tree.h +++ b/src/ast/substitution/substitution_tree.h @@ -29,7 +29,7 @@ class st_visitor { substitution & m_subst; public: st_visitor(substitution & s):m_subst(s) {} - virtual ~st_visitor() {} + virtual ~st_visitor() = default; substitution & get_substitution() { return m_subst; } virtual bool operator()(expr * e) { return true; } }; diff --git a/src/ast/value_generator.h b/src/ast/value_generator.h index 7b77b144ea7..f3a45938973 100644 --- a/src/ast/value_generator.h +++ b/src/ast/value_generator.h @@ -23,7 +23,7 @@ class value_generator_core { public: - virtual ~value_generator_core() {} + virtual ~value_generator_core() = default; virtual family_id get_fid() const = 0; virtual expr_ref get_value(sort* s, unsigned index) = 0; }; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 3dc49624bb0..d54a9014376 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -96,7 +96,7 @@ class macro_decls { class object_ref { unsigned m_ref_count = 0; public: - virtual ~object_ref() {} + virtual ~object_ref() = default; virtual void finalize(cmd_context & ctx) = 0; void inc_ref(cmd_context & ctx) { m_ref_count++; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 5c7058bb532..b8dd01aea64 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -781,7 +781,7 @@ struct pdecl_manager::sort_info { m_decl(d) { m.inc_ref(d); } - virtual ~sort_info() {} + virtual ~sort_info() = default; virtual unsigned obj_size() const { return sizeof(sort_info); } virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); } virtual void display(std::ostream & out, pdecl_manager const & m) const = 0; diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 66e1e5e8152..a55f782f0c6 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -38,7 +38,7 @@ class pdecl { virtual size_t obj_size() const { UNREACHABLE(); return sizeof(*this); } pdecl(unsigned id, unsigned num_params):m_id(id), m_num_params(num_params), m_ref_count(0) {} virtual void finalize(pdecl_manager & m) {} - virtual ~pdecl() {} + virtual ~pdecl() = default; public: virtual bool check_num_params(pdecl * other) const { return m_num_params == other->m_num_params; } unsigned get_num_params() const { return m_num_params; } @@ -257,7 +257,7 @@ class pdatatypes_decl : public pdecl { class new_datatype_eh { public: - virtual ~new_datatype_eh() {} + virtual ~new_datatype_eh() = default; virtual void operator()(sort * dt, pdecl* pd) = 0; }; diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h index 8c1ca55e668..a642ceb417c 100644 --- a/src/math/automata/boolean_algebra.h +++ b/src/math/automata/boolean_algebra.h @@ -25,7 +25,7 @@ Revision History: template class positive_boolean_algebra { public: - virtual ~positive_boolean_algebra() {} + virtual ~positive_boolean_algebra() = default; virtual T mk_false() = 0; virtual T mk_true() = 0; virtual T mk_and(T x, T y) = 0; diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h index fcdce7311f6..b492fb7ee44 100644 --- a/src/math/hilbert/heap_trie.h +++ b/src/math/hilbert/heap_trie.h @@ -66,7 +66,7 @@ class heap_trie { unsigned m_ref; public: node(node_t t): m_type(t), m_ref(0) {} - virtual ~node() {} + virtual ~node() = default; node_t type() const { return m_type; } void inc_ref() { ++m_ref; } void dec_ref() { SASSERT(m_ref > 0); --m_ref; } diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 3bcd62d00bf..8e6311683b5 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -57,7 +57,7 @@ class lar_base_constraint { virtual vector> coeffs() const = 0; lar_base_constraint(unsigned j, lconstraint_kind kind, const mpq& right_side) :m_kind(kind), m_right_side(right_side), m_active(false), m_j(j) {} - virtual ~lar_base_constraint() {} + virtual ~lar_base_constraint() = default; lconstraint_kind kind() const { return m_kind; } mpq const& rhs() const { return m_right_side; } diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 8c05f8354c3..2a4e5058d4f 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -49,7 +49,7 @@ namespace lp_api { m_constraints[1] = ct; } - virtual ~bound() {} + virtual ~bound() = default; theory_var get_var() const { return m_var; } diff --git a/src/math/lp/matrix.h b/src/math/lp/matrix.h index 80ddb12287c..88a405614ff 100644 --- a/src/math/lp/matrix.h +++ b/src/math/lp/matrix.h @@ -22,7 +22,7 @@ class matrix { virtual void set_number_of_rows(unsigned m) = 0; virtual void set_number_of_columns(unsigned n) = 0; - virtual ~matrix() {} + virtual ~matrix() = default; bool is_equal(const matrix& other); bool operator == (matrix const & other) { diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 083b935a4ca..e4087a407fd 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -85,7 +85,7 @@ class nex { bool is_scalar() const { return type() == expr_type::SCALAR; } virtual bool is_pure_monomial() const { return false; } std::string str() const { std::stringstream ss; print(ss); return ss.str(); } - virtual ~nex() {} + virtual ~nex() = default; virtual bool contains(lpvar j) const { return false; } virtual unsigned get_degree() const = 0; // simplifies the expression and also assigns the address of "this" to *e diff --git a/src/math/lp/tail_matrix.h b/src/math/lp/tail_matrix.h index 2047e8c7e9b..9fa1a4a4782 100644 --- a/src/math/lp/tail_matrix.h +++ b/src/math/lp/tail_matrix.h @@ -37,7 +37,7 @@ class tail_matrix virtual void apply_from_left(vector & w, lp_settings & settings) = 0; virtual void apply_from_right(vector & w) = 0; virtual void apply_from_right(indexed_vector & w) = 0; - virtual ~tail_matrix() {} + virtual ~tail_matrix() = default; virtual bool is_dense() const = 0; struct ref_row { const tail_matrix & m_A; diff --git a/src/math/simplex/network_flow.h b/src/math/simplex/network_flow.h index 9be3b1191e2..b2c9cd9b3c4 100644 --- a/src/math/simplex/network_flow.h +++ b/src/math/simplex/network_flow.h @@ -87,7 +87,7 @@ namespace smt { m_states(states), m_enter_id(enter_id) { } - virtual ~pivot_rule_impl() {} + virtual ~pivot_rule_impl() = default; virtual bool choose_entering_edge() = 0; virtual pivot_rule rule() const = 0; }; diff --git a/src/math/subpaving/subpaving.h b/src/math/subpaving/subpaving.h index 96d05f4def0..b76f5e83134 100644 --- a/src/math/subpaving/subpaving.h +++ b/src/math/subpaving/subpaving.h @@ -39,7 +39,7 @@ namespace subpaving { class context { public: - virtual ~context() {} + virtual ~context() = default; virtual unsynch_mpq_manager & qm() const = 0; diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index cfe3aea70d1..7300e3da3c4 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -385,7 +385,7 @@ class context_t { context_t * m_ctx; public: node_selector(context_t * ctx):m_ctx(ctx) {} - virtual ~node_selector() {} + virtual ~node_selector() = default; context_t * ctx() const { return m_ctx; } @@ -403,7 +403,7 @@ class context_t { context_t * m_ctx; public: var_selector(context_t * ctx):m_ctx(ctx) {} - virtual ~var_selector() {} + virtual ~var_selector() = default; context_t * ctx() const { return m_ctx; } @@ -436,7 +436,7 @@ class context_t { context_t * m_ctx; public: node_splitter(context_t * ctx):m_ctx(ctx) {} - virtual ~node_splitter() {} + virtual ~node_splitter() = default; context_t * ctx() const { return m_ctx; } node * mk_node(node * p) { return ctx()->mk_node(p); } diff --git a/src/model/model_macro_solver.h b/src/model/model_macro_solver.h index 1c04f8ec17b..8070b4adaad 100644 --- a/src/model/model_macro_solver.h +++ b/src/model/model_macro_solver.h @@ -20,7 +20,7 @@ Copyright (c) 2006 Microsoft Corporation class quantifier2macro_infos { public: - virtual ~quantifier2macro_infos() {} + virtual ~quantifier2macro_infos() = default; virtual quantifier_macro_info* operator()(quantifier* q) = 0; }; @@ -48,7 +48,7 @@ class base_macro_solver { m_model(nullptr) { } - virtual ~base_macro_solver() {} + virtual ~base_macro_solver() = default; /** \brief Try to satisfy quantifiers in qs by using macro definitions. diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f6ce3951802..4efe79dd3d5 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -53,7 +53,7 @@ namespace datalog { m_limited_size = ctx.get_decl_util().try_get_size(s, m_size); } public: - virtual ~sort_domain() {} + virtual ~sort_domain() = default; sort_kind get_kind() const { return m_kind; } virtual unsigned get_constant_count() const = 0; diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index fcf45abf93a..64218f7d6b8 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -42,7 +42,7 @@ namespace datalog { std::string m_name; public: engine_base(ast_manager& m, char const* name): m(m), m_name(name) {} - virtual ~engine_base() {} + virtual ~engine_base() = default; virtual expr_ref get_answer() = 0; virtual expr_ref get_ground_sat_answer () { diff --git a/src/muz/base/dl_rule_transformer.h b/src/muz/base/dl_rule_transformer.h index 59eb24f55b9..c446593bddf 100644 --- a/src/muz/base/dl_rule_transformer.h +++ b/src/muz/base/dl_rule_transformer.h @@ -89,7 +89,7 @@ namespace datalog { m_can_destratify_negation(can_destratify_negation), m_transformer(nullptr) {} public: - virtual ~plugin() {} + virtual ~plugin() = default; unsigned get_priority() { return m_priority; } bool can_destratify_negation() const { return m_can_destratify_negation; } diff --git a/src/muz/fp/datalog_parser.h b/src/muz/fp/datalog_parser.h index 2369f1d8491..e836cbaec83 100644 --- a/src/muz/fp/datalog_parser.h +++ b/src/muz/fp/datalog_parser.h @@ -27,7 +27,7 @@ namespace datalog { public: static parser * create(context& ctx, ast_manager & ast_manager); - virtual ~parser() {} + virtual ~parser() = default; virtual bool parse_file(char const * path) = 0; virtual bool parse_string(char const * string) = 0; @@ -37,7 +37,7 @@ namespace datalog { public: static wpa_parser * create(context& ctx, ast_manager & ast_manager); - virtual ~wpa_parser() {} + virtual ~wpa_parser() = default; virtual bool parse_directory(char const * path) = 0; }; diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 376b41d3473..ea317ca4554 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -179,7 +179,7 @@ namespace datalog { class base_fn { public: base_fn() = default; - virtual ~base_fn() {} + virtual ~base_fn() = default; base_fn(const base_fn &) = delete; base_fn& operator=(const base_fn &) = delete; @@ -260,7 +260,7 @@ namespace datalog { */ bool check_kind(base_object const& r) const { return &r.get_plugin()==this; } public: - virtual ~plugin_object() {} + virtual ~plugin_object() = default; virtual void initialize(family_id fid) { m_kind = fid; } @@ -423,7 +423,7 @@ namespace datalog { } #endif - virtual ~base_ancestor() {} + virtual ~base_ancestor() = default; void set_kind(family_id kind) { SASSERT(kind>=0); m_kind = kind; } @@ -865,7 +865,7 @@ namespace datalog { class table_row_mutator_fn { public: - virtual ~table_row_mutator_fn() {} + virtual ~table_row_mutator_fn() = default; /** \brief The function is called for a particular table row. The \c func_columns contains a pointer to an array of functional column values that can be modified. If the function @@ -879,7 +879,7 @@ namespace datalog { class table_row_pair_reduce_fn { public: - virtual ~table_row_pair_reduce_fn() {} + virtual ~table_row_pair_reduce_fn() = default; /** \brief The function is called for pair of table rows that became duplicated due to projection. The values that are in the first array after return from the function will be used for the @@ -1095,7 +1095,7 @@ namespace datalog { unsigned m_ref_cnt; public: iterator_core() : m_ref_cnt(0) {} - virtual ~iterator_core() {} + virtual ~iterator_core() = default; iterator_core(const iterator_core &) = delete; iterator_core & operator=(const iterator_core &) = delete; @@ -1124,7 +1124,7 @@ namespace datalog { unsigned m_ref_cnt; public: row_iterator_core() : m_ref_cnt(0) {} - virtual ~row_iterator_core() {} + virtual ~row_iterator_core() = default; row_iterator_core(const row_iterator_core &) = delete; row_iterator_core & operator=(const row_iterator_core &) = delete; @@ -1205,7 +1205,7 @@ namespace datalog { typedef row_iterator const_iterator; row_interface(const table_base & parent_table) : m_parent_table(parent_table) {} - virtual ~row_interface() {} + virtual ~row_interface() = default; virtual table_element operator[](unsigned col) const = 0; diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h index 4b56894650b..17e9a236462 100644 --- a/src/muz/rel/dl_external_relation.h +++ b/src/muz/rel/dl_external_relation.h @@ -26,7 +26,7 @@ namespace datalog { class external_relation_context { public: - virtual ~external_relation_context() {} + virtual ~external_relation_context() = default; virtual family_id get_family_id() const = 0; diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 1edacc94fd8..a008c2b731e 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -317,7 +317,7 @@ namespace datalog { class instruction_block { public: struct instruction_observer { - virtual ~instruction_observer() {} + virtual ~instruction_observer() = default; virtual void notify(instruction * i) {} }; private: diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h index 56bfc961f77..9f88e6aa2b5 100644 --- a/src/muz/rel/dl_lazy_table.h +++ b/src/muz/rel/dl_lazy_table.h @@ -107,7 +107,7 @@ namespace datalog { public: lazy_table_ref(lazy_table_plugin& p, table_signature const& sig): m_plugin(p), m_signature(sig), m_ref(0) {} - virtual ~lazy_table_ref() {} + virtual ~lazy_table_ref() = default; void inc_ref() { ++m_ref; } void dec_ref() { --m_ref; if (0 == m_ref) dealloc(this); } void release_table() { m_table.release(); } diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index a782cc143ce..9410e2ab023 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -999,7 +999,7 @@ namespace datalog { class relation_manager::auxiliary_table_transformer_fn { table_fact m_row; public: - virtual ~auxiliary_table_transformer_fn() {} + virtual ~auxiliary_table_transformer_fn() = default; virtual const table_signature & get_result_signature() const = 0; virtual void modify_fact(table_fact & f) const = 0; @@ -1241,7 +1241,7 @@ namespace datalog { table_fact m_row; svector m_to_remove; public: - virtual ~auxiliary_table_filter_fn() {} + virtual ~auxiliary_table_filter_fn() = default; virtual bool should_remove(const table_fact & f) const = 0; void operator()(table_base & r) { diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index 9f3304e7ae1..6c2373d54b4 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -274,7 +274,7 @@ namespace datalog { key_indexer(unsigned key_len, const unsigned * key_cols) : m_key_cols(key_len, key_cols) {} - virtual ~key_indexer() {} + virtual ~key_indexer() = default; virtual void update(const sparse_table & t) {} diff --git a/src/muz/rel/dl_table_plugin.h b/src/muz/rel/dl_table_plugin.h index 51e54d3ea0e..d0f239f7989 100644 --- a/src/muz/rel/dl_table_plugin.h +++ b/src/muz/rel/dl_table_plugin.h @@ -40,7 +40,7 @@ namespace datalog { class base_fn { public: - virtual ~base_fn() {} + virtual ~base_fn() = default; }; class join_fn : public base_fn { @@ -113,7 +113,7 @@ namespace datalog { base_ancestor(kind k, relation_manager & m, const signature & s) : m_kind(k), m_manager(m), m_signature(s) {} public: - virtual ~base_ancestor() {} + virtual ~base_ancestor() = default; kind get_kind() const { return m_kind; } relation_manager & get_manager() const { return m_manager; } diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index b62da076625..6ef56c737db 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -857,7 +857,7 @@ class lemma_generalizer { context& m_ctx; public: lemma_generalizer(context& ctx): m_ctx(ctx) {} - virtual ~lemma_generalizer() {} + virtual ~lemma_generalizer() = default; virtual void operator()(lemma_ref &lemma) = 0; virtual void collect_statistics(statistics& st) const {} virtual void reset_statistics() {} diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index 581a877cfb6..a7ea4c89bb6 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/src/muz/spacer/spacer_unsat_core_plugin.h @@ -31,7 +31,7 @@ namespace spacer { ast_manager& m; public: unsat_core_plugin(unsat_core_learner& learner); - virtual ~unsat_core_plugin() {}; + virtual ~unsat_core_plugin() = default; virtual void compute_partial_core(proof* step) = 0; virtual void finalize(){}; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 72195467f45..ac39d78913a 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -42,7 +42,7 @@ namespace opt { class maxsmt_solver { public: - virtual ~maxsmt_solver() {} + virtual ~maxsmt_solver() = default; virtual lbool operator()() = 0; virtual rational get_lower() const = 0; virtual rational get_upper() const = 0; diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h index 8e16ec5c8d1..1bc27f9b132 100644 --- a/src/opt/opt_lns.h +++ b/src/opt/opt_lns.h @@ -28,7 +28,7 @@ namespace opt { class lns_context { public: - virtual ~lns_context() {} + virtual ~lns_context() = default; virtual void update_model(model_ref& mdl) = 0; virtual void relax_cores(vector const& cores) = 0; virtual rational cost(model& mdl) = 0; diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h index ab5a90237e8..105f4007f1f 100644 --- a/src/opt/opt_pareto.h +++ b/src/opt/opt_pareto.h @@ -52,7 +52,7 @@ namespace opt { m_solver(s), m_params(p) { } - virtual ~pareto_base() {} + virtual ~pareto_base() = default; virtual void updt_params(params_ref & p) { m_solver->updt_params(p); m_params.copy(p); diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index 5256dd47abf..2867f52a3ca 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -55,7 +55,7 @@ namespace opt { { updt_params(p); } - virtual ~sls_solver() {} + virtual ~sls_solver() = default; virtual void updt_params(params_ref & p) { m_solver->updt_params(p); diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 12b59296038..4f73b92e635 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -59,7 +59,7 @@ namespace mbp { public: project_plugin(ast_manager& m) :m(m), m_cache(m), m_args(m), m_pure_eqs(m) {} - virtual ~project_plugin() {} + virtual ~project_plugin() = default; virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; } /** \brief partial solver. diff --git a/src/qe/mbp/mbp_solve_plugin.h b/src/qe/mbp/mbp_solve_plugin.h index 27e7f85a812..2450eab4ffe 100644 --- a/src/qe/mbp/mbp_solve_plugin.h +++ b/src/qe/mbp/mbp_solve_plugin.h @@ -36,7 +36,7 @@ namespace mbp { bool is_variable(expr* e) const { return m_is_var(e); } public: solve_plugin(ast_manager& m, family_id fid, is_variable_proc& is_var) : m(m), m_id(fid), m_is_var(is_var) {} - virtual ~solve_plugin() {} + virtual ~solve_plugin() = default; family_id get_family_id() const { return m_id; } /// Process (and potentially augment) a literal expr_ref operator() (expr *lit); diff --git a/src/qe/nlarith_util.h b/src/qe/nlarith_util.h index acbe4889e28..dccc4f606fa 100644 --- a/src/qe/nlarith_util.h +++ b/src/qe/nlarith_util.h @@ -116,7 +116,7 @@ namespace nlarith { class eval { public: - virtual ~eval() {} + virtual ~eval() = default; virtual lbool operator()(app* a) = 0; }; @@ -124,7 +124,7 @@ namespace nlarith { class branch { public: - virtual ~branch() {} + virtual ~branch() = default; virtual app* get_constraint() = 0; virtual void get_updates(ptr_vector& atoms, svector& updates) = 0; }; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 509b73835cc..d859880d811 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -877,7 +877,7 @@ namespace qe { class quant_elim { public: - virtual ~quant_elim() {} + virtual ~quant_elim() = default; virtual lbool eliminate_exists( unsigned num_vars, app* const* vars, diff --git a/src/qe/qe.h b/src/qe/qe.h index a5152522f37..55729d0b5a8 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -149,7 +149,7 @@ namespace qe { m_ctx(ctx) {} - virtual ~qe_solver_plugin() {} + virtual ~qe_solver_plugin() = default; family_id get_family_id() { return m_fid; } diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index e3582281317..70c0f98bb68 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -43,7 +43,7 @@ namespace qe { lbool is_shared_cached(expr* e); public: mbi_plugin(ast_manager& m): m(m), m_shared_trail(m) {} - virtual ~mbi_plugin() {} + virtual ~mbi_plugin() = default; /** * Set the shared symbols. diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 1bb37b7d7ce..ffcb9558718 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -70,7 +70,7 @@ namespace sat { solver* m_solver { nullptr }; public: extension(symbol const& name, int id): m_id(id), m_name(name) { } - virtual ~extension() {} + virtual ~extension() = default; int get_id() const { return m_id; } void set_solver(solver* s) { m_solver = s; } solver& s() { return *m_solver; } diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 407deae5cc1..5c8b7e315db 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -31,7 +31,7 @@ namespace sat { reslimit& m_rlimit; public: solver_core(reslimit& l) : m_rlimit(l) {} - virtual ~solver_core() {} + virtual ~solver_core() = default; // add clauses virtual void add_clause(unsigned n, literal* lits, status st) = 0; diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index fa42f0712ee..db13db054a0 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -80,7 +80,7 @@ namespace sat { class i_local_search { public: - virtual ~i_local_search() {} + virtual ~i_local_search() = default; virtual void add(solver const& s) = 0; virtual void updt_params(params_ref const& p) = 0; virtual void set_seed(unsigned s) = 0; diff --git a/src/sat/smt/q_mam.h b/src/sat/smt/q_mam.h index c396a319bce..9fc6d18f18f 100644 --- a/src/sat/smt/q_mam.h +++ b/src/sat/smt/q_mam.h @@ -45,7 +45,7 @@ namespace q { static mam * mk(euf::solver& ctx, ematch& em); - virtual ~mam() {} + virtual ~mam() = default; virtual void add_pattern(quantifier * q, app * mp) = 0; diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index 9653268e614..2c16504c6e7 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -43,7 +43,7 @@ namespace q { ast_manager& m; public: projection_function(ast_manager& m) : m(m) {} - virtual ~projection_function() {} + virtual ~projection_function() = default; virtual expr* mk_lt(expr* a, expr* b) = 0; expr* mk_le(expr* a, expr* b) { return m.mk_not(mk_lt(b, a)); } virtual bool operator()(expr* a, expr* b) const = 0; diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h index 43413a8930f..e7d0d9b431c 100644 --- a/src/sat/smt/sat_internalizer.h +++ b/src/sat/smt/sat_internalizer.h @@ -21,7 +21,7 @@ Module Name: namespace sat { class sat_internalizer { public: - virtual ~sat_internalizer() {} + virtual ~sat_internalizer() = default; virtual bool is_bool_op(expr* e) const = 0; virtual literal internalize(expr* e, bool learned) = 0; virtual bool_var to_bool_var(expr* e) = 0; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 7209fa0512a..833b6c05e72 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -39,7 +39,7 @@ namespace euf { virtual bool post_visit(expr* e, bool sign, bool root) { return false; } public: - virtual ~th_internalizer() {} + virtual ~th_internalizer() = default; virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0; @@ -60,7 +60,7 @@ namespace euf { class th_decompile { public: - virtual ~th_decompile() {} + virtual ~th_decompile() = default; virtual bool to_formulas(std::function& lit2expr, expr_ref_vector& fmls) { return false; } }; @@ -68,7 +68,7 @@ namespace euf { class th_model_builder { public: - virtual ~th_model_builder() {} + virtual ~th_model_builder() = default; /** \brief compute the value for enode \c n and store the value in \c values diff --git a/src/smt/mam.h b/src/smt/mam.h index bf23b24a6eb..e7051b3f766 100644 --- a/src/smt/mam.h +++ b/src/smt/mam.h @@ -37,8 +37,7 @@ namespace smt { m_context(ctx) { } - virtual ~mam() { - } + virtual ~mam() = default; virtual void add_pattern(quantifier * q, app * mp) = 0; diff --git a/src/smt/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h index 91f7fc036a4..a84b5ea4f8d 100644 --- a/src/smt/smt_case_split_queue.h +++ b/src/smt/smt_case_split_queue.h @@ -45,7 +45,7 @@ namespace smt { virtual void pop_scope(unsigned num_scopes) = 0; virtual void next_case_split(bool_var & next, lbool & phase) = 0; virtual void display(std::ostream & out) = 0; - virtual ~case_split_queue() {} + virtual ~case_split_queue() = default; // theory-aware branching hint virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {} diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index 950d0e17c4c..89d8f2d66bc 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -33,7 +33,7 @@ namespace smt { */ class clause_del_eh { public: - virtual ~clause_del_eh() {} + virtual ~clause_del_eh() = default; virtual void operator()(ast_manager & m, clause * cls) = 0; }; diff --git a/src/smt/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h index 4b4492b7f33..20be165c67a 100644 --- a/src/smt/smt_for_each_relevant_expr.h +++ b/src/smt/smt_for_each_relevant_expr.h @@ -65,7 +65,7 @@ namespace smt { public: for_each_relevant_expr(context & ctx); - virtual ~for_each_relevant_expr() {} + virtual ~for_each_relevant_expr() = default; /** \brief Visit the relevant sub-expressions of n. That is, only subexpressions m of n, such that m_context.is_relevant(m). diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index b90233792d4..b13d127436d 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -49,7 +49,7 @@ namespace smt { unsigned m_in_region:1; // true if the object was allocated in a region. public: justification(bool in_region = true):m_mark(false), m_in_region(in_region) {} - virtual ~justification() {} + virtual ~justification() = default; /** \brief This method should return true if the method del_eh needs to be invoked diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 24ec4d5b960..94a0992f3ba 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1157,7 +1157,7 @@ namespace smt { ast_manager& m; public: qinfo(ast_manager& m) :m(m) {} - virtual ~qinfo() {} + virtual ~qinfo() = default; virtual char const* get_kind() const = 0; virtual bool is_equal(qinfo const* qi) const = 0; virtual void display(std::ostream& out) const { out << "[" << get_kind() << "]"; } diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h index 80bd59799fa..632557e9833 100644 --- a/src/smt/smt_model_generator.h +++ b/src/smt/smt_model_generator.h @@ -136,7 +136,7 @@ namespace smt { */ class model_value_proc { public: - virtual ~model_value_proc() {} + virtual ~model_value_proc() = default; /** \brief Fill result with the dependencies of this functor. That is, to invoke mk_value, the dependencies in result must be constructed. diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index d9a43ddeadc..abb3cac7c6b 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -106,7 +106,7 @@ namespace smt { class quantifier_manager_plugin { public: - virtual ~quantifier_manager_plugin() {} + virtual ~quantifier_manager_plugin() = default; virtual void set_manager(quantifier_manager & qm) = 0; diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index 87cc3847cd1..f64b7d05973 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -29,7 +29,7 @@ namespace smt { void mark_as_relevant(relevancy_propagator & rp, expr * n); void mark_args_as_relevant(relevancy_propagator & rp, app * n); public: - virtual ~relevancy_eh() {} + virtual ~relevancy_eh() = default; /** \brief This method is invoked when n is marked as relevant. */ @@ -87,7 +87,7 @@ namespace smt { context & m_context; public: relevancy_propagator(context & ctx); - virtual ~relevancy_propagator() {} + virtual ~relevancy_propagator() = default; context & get_context() { return m_context; } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index af7b97c72cb..32a9314f0ad 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -294,7 +294,7 @@ namespace smt { m_bound_kind(k), m_atom(a) { } - virtual ~bound() {} + virtual ~bound() = default; theory_var get_var() const { return m_var; } bound_kind get_bound_kind() const { return static_cast(m_bound_kind); } bool is_atom() const { return m_atom; } diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index e26db51d0a7..5a5e1e6f2ab 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -42,7 +42,7 @@ namespace smt { class atom { public: - virtual ~atom() {} + virtual ~atom() = default; virtual bool is_bit() const = 0; }; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index fb5a821d5dc..48acb6ad8a0 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -222,7 +222,7 @@ namespace smt { class apply { public: - virtual ~apply() {} + virtual ~apply() = default; virtual void operator()(theory_seq& th) = 0; }; diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 53ffd2a1d5f..86941f590a8 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -45,7 +45,7 @@ class check_sat_result { double m_time; public: check_sat_result():m_ref_count(0), m_status(l_undef), m_time(0) {} - virtual ~check_sat_result() {} + virtual ~check_sat_result() = default; void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } lbool set_status(lbool r) { return m_status = r; } diff --git a/src/solver/progress_callback.h b/src/solver/progress_callback.h index e8c46360997..f49609dafe4 100644 --- a/src/solver/progress_callback.h +++ b/src/solver/progress_callback.h @@ -20,7 +20,7 @@ Revision History: class progress_callback { public: - virtual ~progress_callback() {} + virtual ~progress_callback() = default; // Called on every check for resource limit exceeded (much more frequent). virtual void fast_progress_sample() {} diff --git a/src/solver/solver.h b/src/solver/solver.h index 09daf3b29f5..8b7d56a8c13 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -29,7 +29,7 @@ class model_converter; class solver_factory { public: - virtual ~solver_factory() {} + virtual ~solver_factory() = default; virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0; }; @@ -113,7 +113,7 @@ class solver : public check_sat_result, public user_propagator::core { virtual void set_phase(expr* e) = 0; virtual void move_to_front(expr* e) = 0; - class phase { public: virtual ~phase() {} }; + class phase { public: virtual ~phase() = default; }; virtual phase* get_phase() = 0; diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index b0e6be1bdf3..3a2f8583125 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -147,7 +147,7 @@ class bv_bound_chk_tactic::imp { imp(ast_manager & m, params_ref const & p, bv_bound_chk_stats& stats) : m_rw(m, p, stats) { } - virtual ~imp() { } + virtual ~imp() = default; ast_manager& m() { return m_rw.m(); } diff --git a/src/tactic/converter.h b/src/tactic/converter.h index 60602557e8e..bbd30c351e5 100644 --- a/src/tactic/converter.h +++ b/src/tactic/converter.h @@ -26,7 +26,7 @@ class converter { unsigned m_ref_count; public: converter():m_ref_count(0) {} - virtual ~converter() {} + virtual ~converter() = default; void inc_ref() { ++m_ref_count; } diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 0beced06e68..c8e34f33d08 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -26,7 +26,7 @@ class ctx_simplify_tactic : public tactic { class simplifier { goal_num_occurs* m_occs; public: - virtual ~simplifier() {} + virtual ~simplifier() = default; virtual bool assert_expr(expr * t, bool sign) = 0; virtual bool simplify(expr* t, expr_ref& result) = 0; virtual bool may_simplify(expr* t) { return true; } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index b5d5e1ce901..43e13d9610c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -64,7 +64,7 @@ class expr_dominators { class dom_simplifier { public: - virtual ~dom_simplifier() {} + virtual ~dom_simplifier() = default; /** \brief assert_expr performs an implicit push */ diff --git a/src/tactic/probe.h b/src/tactic/probe.h index ae287916365..4d1af66a8a9 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -44,7 +44,7 @@ class probe { public: probe():m_ref_count(0) {} - virtual ~probe() {} + virtual ~probe() = default; 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/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 46b5eda8a14..18d71b51472 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -53,7 +53,7 @@ namespace user_propagator { class core { public: - virtual ~core() {} + virtual ~core() = default; virtual void user_propagate_init( void* ctx, diff --git a/src/test/ex.cpp b/src/test/ex.cpp index 44443147568..10b5f8a90e9 100644 --- a/src/test/ex.cpp +++ b/src/test/ex.cpp @@ -21,7 +21,7 @@ Revision History: class ex { public: - virtual ~ex() {} + virtual ~ex() = default; virtual char const * msg() const = 0; }; diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h index 5195333fc06..b8c3d475837 100644 --- a/src/util/cmd_context_types.h +++ b/src/util/cmd_context_types.h @@ -87,7 +87,7 @@ class cmd { int m_pos; public: cmd(char const * n):m_name(n), m_line(0), m_pos(0) {} - virtual ~cmd() {} + virtual ~cmd() = default; virtual void reset(cmd_context & ctx) {} virtual void finalize(cmd_context & ctx) {} virtual symbol get_name() const { return m_name; } diff --git a/src/util/event_handler.h b/src/util/event_handler.h index 8993162e6ba..cabbca4c93d 100644 --- a/src/util/event_handler.h +++ b/src/util/event_handler.h @@ -31,7 +31,7 @@ class event_handler { event_handler_caller_t m_caller_id; public: event_handler(): m_caller_id(UNSET_EH_CALLER) {} - virtual ~event_handler() {} + virtual ~event_handler() = default; virtual void operator()(event_handler_caller_t caller_id) = 0; event_handler_caller_t caller_id() const { return m_caller_id; } }; diff --git a/src/util/trail.h b/src/util/trail.h index 9a7ec4303a4..20a525cf7bd 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -26,7 +26,7 @@ Revision History: class trail { public: - virtual ~trail() {} + virtual ~trail() = default; virtual void undo() = 0; }; diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h index 1d54fb7b5a1..b6875257c79 100644 --- a/src/util/z3_exception.h +++ b/src/util/z3_exception.h @@ -22,7 +22,7 @@ Module Name: class z3_exception { public: - virtual ~z3_exception() {} + virtual ~z3_exception() = default; virtual char const * msg() const = 0; virtual unsigned error_code() const; bool has_error_code() const;