diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index f71e7d232..ae02e371e 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -63,7 +63,6 @@ class scoped_expr_substitution { public: scoped_expr_substitution(expr_substitution& s): m_subst(s), m_trail(s.m()) {} - ~scoped_expr_substitution() {} void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr) { if (!m_subst.contains(s)) { diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index aa51c9e47..1cc6b7461 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -127,9 +127,6 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { updt_params(p); } - ~blaster_rewriter_cfg() { - } - void updt_params(params_ref const & p) { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_steps = p.get_uint("max_steps", UINT_MAX); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index c53df0c41..15aaa7672 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -27,9 +27,6 @@ fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : updt_params(p); } -fpa_rewriter::~fpa_rewriter() { -} - void fpa_rewriter::updt_params(params_ref const & _p) { fpa_rewriter_params p(_p); m_hi_fp_unspecified = p.hi_fp_unspecified(); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index b80bee09d..333302eec 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -38,7 +38,6 @@ class fpa_rewriter { public: fpa_rewriter(ast_manager & m, params_ref const & p = params_ref()); - ~fpa_rewriter(); ast_manager & m() const { return m_util.m(); } family_id get_fid() const { return m_util.get_fid(); } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 65cf5d805..2c04d962f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -235,8 +235,6 @@ public: re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {} -re2automaton::~re2automaton() {} - void re2automaton::set_solver(expr_solver* solver) { m_solver = solver; m_ba = alloc(sym_expr_boolean_algebra, m, *solver); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 296485d73..122e50eb8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -103,7 +103,6 @@ class re2automaton { eautomaton* seq2aut(expr* e); public: re2automaton(ast_manager& m); - ~re2automaton(); eautomaton* operator()(expr* e); void set_solver(expr_solver* solver); bool has_solver() const { return m_solver; } diff --git a/src/model/model.cpp b/src/model/model.cpp index d7b96a902..83d13f703 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -221,8 +221,6 @@ struct model::top_sort : public ::top_sort { m_occur_count.find(f, count); return count; } - - ~top_sort() override {} }; void model::compress() { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index d5d05c368..9683e121e 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -39,8 +39,6 @@ public: SASSERT(m_t2); } - ~binary_tactical() override { } - void updt_params(params_ref const & p) override { m_t1->updt_params(p); m_t2->updt_params(p); @@ -101,7 +99,6 @@ struct false_pred { class and_then_tactical : public binary_tactical { public: and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {} - ~and_then_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer& result) override { @@ -232,8 +229,6 @@ public: } } - ~nary_tactical() override { } - void updt_params(params_ref const & p) override { TRACE("nary_tactical_updt_params", tout << "updt_params: " << p << "\n";); for (tactic* t : m_ts) t->updt_params(p); @@ -284,8 +279,6 @@ class or_else_tactical : public nary_tactical { public: or_else_tactical(unsigned num, tactic * const * ts):nary_tactical(num, ts) { SASSERT(num > 0); } - ~or_else_tactical() override {} - void operator()(goal_ref const & in, goal_ref_buffer& result) override { goal orig(*(in.get())); unsigned sz = m_ts.size(); @@ -386,9 +379,6 @@ public: par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) { error_code = 0; } - ~par_tactical() override {} - - void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; @@ -525,7 +515,6 @@ tactic * par_and_then(tactic * t1, tactic * t2) { class par_and_then_tactical : public and_then_tactical { public: par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {} - ~par_and_then_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; @@ -780,9 +769,7 @@ public: unary_tactical(tactic * t): m_t(t) { SASSERT(t); - } - - ~unary_tactical() override { } + } void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); @@ -1007,7 +994,7 @@ tactic * using_params(tactic * t, params_ref const & p) { class annotate_tactical : public unary_tactical { std::string m_name; struct scope { - std::string m_name; + const std::string &m_name; scope(std::string const& name) : m_name(name) { IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << m_name << " start)\n";); } @@ -1043,8 +1030,6 @@ public: m_p(p) { SASSERT(m_p); } - - ~cond_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (m_p->operator()(*(in.get())).is_true()) @@ -1075,8 +1060,6 @@ public: m_p(p) { SASSERT(m_p); } - - ~fail_if_tactic() override {} void cleanup() override {} diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/tactic/ufbv/ufbv_rewriter.h index 96a3dcf06..d855047a0 100644 --- a/src/tactic/ufbv/ufbv_rewriter.h +++ b/src/tactic/ufbv/ufbv_rewriter.h @@ -91,7 +91,7 @@ The code in spc_rewriter.* does something like that. We cannot reuse this code d for the superposion engine in Z3, but we can adapt it for our needs in the preprocessor. */ -class ufbv_rewriter { +class ufbv_rewriter final { class rewrite_proc; class add_back_idx_proc; class remove_back_idx_proc; @@ -185,17 +185,16 @@ class ufbv_rewriter { void reschedule_processed(func_decl * f); void reschedule_demodulators(func_decl * f, expr * np); unsigned max_var_id(expr * e); - -protected: + // is_smaller returns -1 for e1e2. - virtual int is_smaller(expr * e1, expr * e2) const; + int is_smaller(expr * e1, expr * e2) const; // is_subset returns -1 for e1 subset e2, +1 for e2 subset e1, 0 else. - virtual int is_subset(expr * e1, expr * e2) const; + int is_subset(expr * e1, expr * e2) const; public: ufbv_rewriter(ast_manager & m); - virtual ~ufbv_rewriter(); + ~ufbv_rewriter(); void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);