remove a few trivial destructors so they get inlined

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

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

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();

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

src/ast/rewriter/seq_rewriter.cpp

@@ -235,8 +235,6 @@ class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
 
 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);

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

src/model/model.cpp

@@ -221,8 +221,6 @@ struct model::top_sort : public ::top_sort<func_decl> {
         m_occur_count.find(f, count);
         return count;
     }
-
-    ~top_sort() override {}
 };
 
 void model::compress() {

src/tactic/tactical.cpp

@@ -39,8 +39,6 @@ class binary_tactical : public tactic {
         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 @@ class nary_tactical : public tactic {
         }
     }
 
-    ~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 @@ class par_tactical : public or_else_tactical {
     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 @@ class unary_tactical : public tactic {
     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 @@ class cond_tactical : public binary_tactical {
         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 @@ class fail_if_tactic : public tactic {
         m_p(p) { 
         SASSERT(m_p);
     }
-
-    ~fail_if_tactic() override {}
 
     void cleanup() override {}
 

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 e1<e2, 0 for e1==e2 and +1 for e1>e2.
-    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);