remove default destructors

src/ast/arith_decl_plugin.cpp

@@ -34,9 +34,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
         m_nums(m_amanager) {
     }
 
-    ~algebraic_numbers_wrapper() {
-    }
-
     unsigned mk_id(algebraic_numbers::anum const & val) {
         SASSERT(!m_amanager.is_rational(val));
         unsigned idx = m_id_gen.mk();

src/ast/ast_trail.h

@@ -33,8 +33,7 @@ class ast2ast_trailmap {
 public:
     ast2ast_trailmap(ast_manager& m):
         m_domain(m),
-        m_range(m), 
-        m_map()
+        m_range(m)
     {}
 
     bool find(S* s, T*& t) {

src/ast/datatype_decl_plugin.cpp

@@ -1040,11 +1040,6 @@ namespace datatype {
         return m_family_id;
     }
 
-
-    util::~util() {
-
-    }
-
     ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
         SASSERT(is_datatype(ty));
         ptr_vector<func_decl> * r = nullptr;

src/ast/datatype_decl_plugin.h

@@ -338,7 +338,6 @@ namespace datatype {
 
     public:
         util(ast_manager & m);
-        ~util();
         ast_manager & get_manager() const { return m; }
         // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); 
         bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }

src/ast/expr2polynomial.cpp

@@ -504,9 +504,6 @@ default_expr2polynomial::default_expr2polynomial(ast_manager & am, polynomial::m
     expr2polynomial(am, pm, nullptr) {
 }
 
-default_expr2polynomial::~default_expr2polynomial() {
-}
-
 bool default_expr2polynomial::is_int(polynomial::var x) const {
     return m_is_int[x];
 }

src/ast/expr2polynomial.h

@@ -102,7 +102,6 @@ class default_expr2polynomial : public expr2polynomial {
     bool_vector m_is_int;
 public:
     default_expr2polynomial(ast_manager & am, polynomial::manager & pm);
-    ~default_expr2polynomial() override;
     bool is_int(polynomial::var x) const override;
 protected:
     polynomial::var mk_var(bool is_int) override;

src/ast/fpa/fpa2bv_rewriter.h

@@ -36,9 +36,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
     fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
 
-    ~fpa2bv_rewriter_cfg() {
-    }
-
     void cleanup_buffers() {
         m_out.finalize();
     }

src/ast/fpa_decl_plugin.cpp

@@ -47,9 +47,6 @@ void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
 }
 
-fpa_decl_plugin::~fpa_decl_plugin() {
-}
-
 unsigned fpa_decl_plugin::mk_id(mpf const & v) {
     unsigned new_id = m_id_gen.mk();
     m_values.reserve(new_id+1);
@@ -961,9 +958,6 @@ fpa_util::fpa_util(ast_manager & m):
     m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
 }
 
-fpa_util::~fpa_util() {
-}
-
 sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) {
     parameter ps[2] = { parameter(ebits), parameter(sbits) };
     return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps);

src/ast/fpa_decl_plugin.h

@@ -175,7 +175,6 @@ class fpa_decl_plugin : public decl_plugin {
     bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
     bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
 
-    ~fpa_decl_plugin() override;
     void finalize() override;
 
     decl_plugin * mk_fresh() override;
@@ -216,7 +215,6 @@ class fpa_util {
 
 public:
     fpa_util(ast_manager & m);
-    ~fpa_util();
 
     ast_manager & m() const { return m_manager; }
     mpf_manager & fm() const { return m_plugin->fm(); }

src/ast/macros/cond_macro.h

@@ -39,10 +39,7 @@ class cond_macro {
         m_weight(weight) {
         SASSERT(!m_hint || !m_cond);
     }
-
-    ~cond_macro() {
-    }
-
+
     func_decl * get_f() const { return m_f; }
 
     expr * get_def() const { return m_def; }

src/ast/macros/macro_finder.cpp

@@ -269,9 +269,6 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
     m_autil(m) {
 }
 
-macro_finder::~macro_finder() {
-}
-
 bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps,  expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "starting expand_macros:\n";
           m_macro_manager.display(tout););

src/ast/macros/macro_finder.h

@@ -43,7 +43,6 @@ class macro_finder {
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
-    ~macro_finder();
     void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
     void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
 };

src/ast/macros/macro_manager.cpp

@@ -41,9 +41,6 @@ macro_manager::macro_manager(ast_manager & m):
     m_util.set_forbidden_set(&m_forbidden_set);
 }
 
-macro_manager::~macro_manager() {
-}
-
 void macro_manager::push_scope() {
     m_scopes.push_back(scope());
     scope & s              = m_scopes.back();

src/ast/macros/macro_manager.h

@@ -64,7 +64,6 @@ class macro_manager {
 
 public:
     macro_manager(ast_manager & m);
-    ~macro_manager();
     void copy_to(macro_manager& dst);
     ast_manager & get_manager() const { return m; }
     macro_util & get_util() { return m_util; }

src/ast/macros/quasi_macros.cpp

@@ -31,9 +31,6 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
   m_new_qsorts(m) {
 }
 
-quasi_macros::~quasi_macros() {
-}
-
 void quasi_macros::find_occurrences(expr * e) {
     unsigned j;
     m_todo.reset();

src/ast/macros/quasi_macros.h

@@ -60,7 +60,6 @@ class quasi_macros {
 
 public:
     quasi_macros(ast_manager & m, macro_manager & mm);
-    ~quasi_macros();
 
     /**
        \brief Find pure function macros and apply them.

src/ast/normal_forms/defined_names.cpp

@@ -57,7 +57,7 @@ struct defined_names::impl {
     unsigned_vector m_lims;          //!< Backtracking support.
 
     impl(ast_manager & m, char const * prefix);
-    virtual ~impl();
+    virtual ~impl() = default;
 
     app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
     void cache_new_name(expr * e, app * name);
@@ -90,9 +90,6 @@ defined_names::impl::impl(ast_manager & m, char const * prefix):
         m_z3name = prefix;
 }
 
-defined_names::impl::~impl() {
-}
-
 /**
    \brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
    where sk is a fresh variable name, and x_i's are the free variables of \c e.

src/ast/pattern/expr_pattern_match.cpp

@@ -41,9 +41,6 @@ expr_pattern_match::expr_pattern_match(ast_manager & manager):
     m_manager(manager), m_precompiled(manager) {        
 }
 
-expr_pattern_match::~expr_pattern_match() {
-}
-
 bool 
 expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
     if (m_regs.empty()) {

src/ast/pattern/expr_pattern_match.h

@@ -116,7 +116,6 @@ class expr_pattern_match {
 
  public:
     expr_pattern_match(ast_manager & manager);
-    ~expr_pattern_match();
     bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
     bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
     unsigned initialize(quantifier* qf);

src/ast/recfun_decl_plugin.cpp

@@ -366,9 +366,6 @@ namespace recfun {
           m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
     }
 
-    util::~util() {
-    }
-
     def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) {
         return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
     }

src/ast/recfun_decl_plugin.h

@@ -237,7 +237,6 @@ namespace recfun {
 
     public:
         util(ast_manager &m);
-        ~util();
 
         ast_manager & m() { return m_manager; }
         family_id get_family_id() const { return m_fid; }

src/ast/sls/bvsls_opt_engine.cpp

@@ -28,10 +28,6 @@ bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
     m_best_model = alloc(model, m);
 }
 
-bvsls_opt_engine::~bvsls_opt_engine()
-{    
-}
-
 bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
     expr_ref const & objective, 
     model_ref initial_model, 

src/ast/sls/bvsls_opt_engine.h

@@ -31,7 +31,6 @@ class bvsls_opt_engine : public sls_engine {
 
 public:
     bvsls_opt_engine(ast_manager & m, params_ref const & p);
-    ~bvsls_opt_engine();
 
     class optimization_result {
     public:

src/cmd_context/cmd_context.cpp

@@ -2464,9 +2464,6 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner):
     m_dt_util(owner.m()) {
 }
 
-cmd_context::dt_eh::~dt_eh() {
-}
-
 void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
     TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
     for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {

src/cmd_context/cmd_context.h

@@ -305,7 +305,6 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     public:
         void reset() { m_dt_util.reset(); }
         dt_eh(cmd_context & owner);
-        ~dt_eh() override;
         void operator()(sort * dt, pdecl* pd) override;
     };
 

src/cmd_context/tactic_cmds.cpp

@@ -27,7 +27,6 @@ Module Name:
 #include "ast/ast_smt2_pp.h"
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
-#include "tactic/probe.h"
 #include "solver/check_sat_result.h"
 #include "cmd_context/cmd_context_to_goal.h"
 #include "cmd_context/echo_tactic.h"
@@ -38,9 +37,6 @@ probe_info::probe_info(symbol const & n, char const * d, probe * p):
     m_probe(p) {
 }
 
-probe_info::~probe_info() {
-}
-
 class declare_tactic_cmd : public cmd {
     symbol           m_name;
     sexpr *          m_decl;

src/cmd_context/tactic_cmds.h

@@ -18,12 +18,12 @@ Module Name:
 #pragma once
 
 #include "ast/ast.h"
+#include "tactic/probe.h"
 #include "util/params.h"
 #include "util/cmd_context_types.h"
 #include "util/ref.h"
 
 class tactic;
-class probe;
 
 typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
 
@@ -52,7 +52,6 @@ class probe_info {
     ref<probe>       m_probe;
 public:
     probe_info(symbol const & n, char const * d, probe * p);
-    ~probe_info();
 
     symbol get_name() const { return m_name; }
     char const * get_descr() const { return m_descr; }

src/math/lp/core_solver_pretty_printer.cpp

@@ -21,7 +21,5 @@ Revision History:
 #include "math/lp/core_solver_pretty_printer_def.h"
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
 template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
-template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
 template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out);
-template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer();
 template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print();

src/math/lp/core_solver_pretty_printer.h

@@ -66,7 +66,6 @@ class core_solver_pretty_printer {
 
     void init_costs();
 
-    ~core_solver_pretty_printer();
     void init_rs_width();
 
     T current_column_norm();

src/math/lp/core_solver_pretty_printer_def.h

@@ -67,8 +67,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_co
 
 }
 
-template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
-}
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() {
     m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size());
     for (unsigned i = 0; i < nrows(); i++) {

src/math/polynomial/algebraic_numbers.cpp

@@ -121,9 +121,6 @@ namespace algebraic_numbers {
             m_y = pm().mk_var();
         }
 
-        ~imp() {
-        }
-
         bool acell_inv(algebraic_cell const& c) {
             auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c));
             return s == sign_zero || c.m_sign_lower == (s == sign_neg);

src/math/realclosure/mpz_matrix.cpp

@@ -36,9 +36,6 @@ mpz_matrix_manager::mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_al
     m_allocator(a) {
 }
 
-mpz_matrix_manager::~mpz_matrix_manager() {
-}
-
 void mpz_matrix_manager::mk(unsigned m, unsigned n, mpz_matrix & A) {
     SASSERT(m > 0 && n > 0);
     del(A);

src/math/realclosure/mpz_matrix.h

@@ -63,7 +63,6 @@ class mpz_matrix_manager {
     bool solve_core(mpz_matrix const & A, mpz * b, bool int_solver);
 public:
     mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_allocator & a);
-    ~mpz_matrix_manager();
     unsynch_mpz_manager & nm() const { return m_nm; }
     void mk(unsigned m, unsigned n, mpz_matrix & A);
     void del(mpz_matrix & r);

src/math/realclosure/realclosure.cpp

@@ -410,8 +410,6 @@ namespace realclosure {
             sbuffer<unsigned>  m_szs;        // size of each polynomial in the sequence
         public:
             scoped_polynomial_seq(imp & m):m_seq_coeffs(m) {}
-            ~scoped_polynomial_seq() {
-            }
 
             /**
                \brief Add a new polynomial to the sequence.

src/model/numeral_factory.cpp

@@ -28,9 +28,6 @@ arith_factory::arith_factory(ast_manager & m):
     m_util(m) {
 }
 
-arith_factory::~arith_factory() {
-}
-
 app * arith_factory::mk_num_value(rational const & val, bool is_int) {
     return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
 }
@@ -40,9 +37,6 @@ bv_factory::bv_factory(ast_manager & m):
     m_util(m) {
 }
 
-bv_factory::~bv_factory() {
-}
-
 app * bv_factory::mk_value_core(rational const & val, sort * s) {
     return m_util.mk_numeral(val, s);
 }

src/model/numeral_factory.h

@@ -34,7 +34,6 @@ class arith_factory : public numeral_factory {
 
 public:
     arith_factory(ast_manager & m);
-    ~arith_factory() override;
 
     app * mk_num_value(rational const & val, bool is_int);
 };
@@ -46,7 +45,6 @@ class bv_factory : public numeral_factory {
 
 public:
     bv_factory(ast_manager & m);
-    ~bv_factory() override;
 
     app * mk_num_value(rational const & val, unsigned bv_size);
 };