remove a hundred implicit constructors/destructors

src/api/api_polynomial.h

@@ -28,9 +28,7 @@ namespace api {
         // TODO: add support for caching expressions -> polynomial and back
     public:
         pmanager(reslimit& lim) : m_pm(lim, m_nm) {}
-        ~pmanager() {}
         polynomial::manager & pm() { return m_pm; }
     };
 
-};
-
+}

src/ast/ast.h

@@ -214,12 +214,10 @@ void display_parameters(std::ostream & out, unsigned n, parameter const * p);
    between symbols (family names) and the unique IDs.
 */
 class family_manager {
-    family_id               m_next_id;
+    family_id               m_next_id = 0;
     symbol_table<family_id> m_families;
     svector<symbol>         m_names;
 public:
-    family_manager():m_next_id(0) {}
-
     /**
        \brief Return the family_id for s, a new id is created if !has_family(s)
 
@@ -999,8 +997,8 @@ struct builtin_name {
 */
 class decl_plugin {
 protected:
-    ast_manager * m_manager;
-    family_id     m_family_id;
+    ast_manager * m_manager = nullptr;
+    family_id     m_family_id = null_family_id;
 
     virtual void set_manager(ast_manager * m, family_id id) {
         SASSERT(m_manager == nullptr);
@@ -1024,8 +1022,6 @@ class decl_plugin {
     friend class ast_manager;
 
 public:
-    decl_plugin():m_manager(nullptr), m_family_id(null_family_id) {}
-
     virtual ~decl_plugin() {}
     virtual void finalize() {}
 
@@ -1354,8 +1350,6 @@ class user_sort_plugin : public decl_plugin {
     svector<symbol> m_sort_names;
     dictionary<int> m_name2decl_kind;
 public:
-    user_sort_plugin() {}
-
     sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
     func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                              unsigned arity, sort * const * domain, sort * range) override;
@@ -2450,7 +2444,6 @@ typedef obj_mark<expr> expr_mark;
 class expr_sparse_mark {
     obj_hashtable<expr> m_marked;
 public:
-    expr_sparse_mark() {}
     bool is_marked(expr * n) const { return m_marked.contains(n); }
     void mark(expr * n) { m_marked.insert(n); }
     void mark(expr * n, bool flag) { if (flag) m_marked.insert(n); else m_marked.erase(n); }
@@ -2461,7 +2454,6 @@ template<unsigned IDX>
 class ast_fast_mark {
     ptr_buffer<ast> m_to_unmark;
 public:
-    ast_fast_mark() {}
     ~ast_fast_mark() {
         reset();
     }
@@ -2603,7 +2595,6 @@ class scoped_mark : public ast_mark {
     unsigned_vector m_lim;
 public:
     scoped_mark(ast_manager& m): m_stack(m) {}
-    ~scoped_mark() override {}
     void mark(ast * n, bool flag) override;
     void reset() override;
     void mark(ast * n);
@@ -2644,7 +2635,3 @@ struct parameter_pp {
 inline std::ostream& operator<<(std::ostream& out, parameter_pp const& pp) {
     return pp.m.display(out, pp.p);
 }
-
-
-
-

src/ast/datatype_decl_plugin.h

@@ -105,7 +105,6 @@ namespace datatype {
         class size {
             unsigned m_ref{ 0 };
         public:
-            size() {}
             virtual ~size() { }
             void inc_ref() { ++m_ref; }
             void dec_ref();
@@ -124,7 +123,6 @@ namespace datatype {
         struct offset : public size {
             sort_size m_offset;
             offset(sort_size const& s): m_offset(s) {}
-            ~offset() override {}
             size* subst(obj_map<sort,size*>& S) override { return this; }
             sort_size eval(obj_map<sort, sort_size> const& S) override { return m_offset; }
         };
@@ -152,7 +150,6 @@ namespace datatype {
         struct sparam : public size {
             sort_ref m_param;
             sparam(sort_ref& p): m_param(p) {}
-            ~sparam() override {}
             size* subst(obj_map<sort, size*>& S) override;
             sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
         };

src/ast/rewriter/ast_counter.h

@@ -35,8 +35,6 @@ class counter {
 public:
     typedef map_impl::iterator iterator;
 
-    counter() {}
-
     void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }    
@@ -74,7 +72,6 @@ class var_counter : public counter {
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
-    var_counter() {}
     void count_vars(const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
@@ -86,8 +83,6 @@ class ast_counter {
  public:
     typedef map_impl::iterator iterator;
 
-    ast_counter() {}
-
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }
 

src/ast/rewriter/recfun_rewriter.h

@@ -26,7 +26,6 @@ class recfun_rewriter {
     recfun::util  m_rec;
 public:
     recfun_rewriter(ast_manager& m): m(m), m_rec(m) {}
-    ~recfun_rewriter() {}
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
 

src/ast/seq_decl_plugin.h

@@ -160,7 +160,6 @@ class seq_decl_plugin : public decl_plugin {
 public:
     seq_decl_plugin();
 
-    ~seq_decl_plugin() override {}
     void finalize() override;
 
     bool unicode() const { return get_char_plugin().unicode(); }
@@ -575,8 +574,6 @@ class seq_util {
         re(*this) {
     }
 
-    ~seq_util() {}
-
     family_id get_family_id() const { return m_fid; }
 };
 

src/ast/shared_occs.h

@@ -24,8 +24,6 @@ Revision History:
 class shared_occs_mark {
     ptr_buffer<ast> m_to_unmark;
 public:
-    shared_occs_mark() {}
-
     ~shared_occs_mark() {
         reset();
     }

src/ast/substitution/matcher.h

@@ -36,8 +36,6 @@ class matcher {
     void reset();
 
 public:
-    matcher() {}
-
     /**
        \brief Return true if e2 is an instance of e1.
        In case of success (result is true), it will store the substitution that makes e1 equals to e2 into s.

src/cmd_context/cmd_context.h

@@ -94,9 +94,8 @@ class macro_decls {
    \brief Generic wrapper.
 */
 class object_ref {
-    unsigned m_ref_count;
+    unsigned m_ref_count = 0;
 public:
-    object_ref():m_ref_count(0) {}
     virtual ~object_ref() {}
     virtual void finalize(cmd_context & ctx) = 0;
     void inc_ref(cmd_context & ctx) {

src/math/dd/pdd_eval.h

@@ -26,9 +26,6 @@ class pdd_eval {
     std::function<rational (unsigned)> m_var2val;
 
 public:
-
-    pdd_eval() {}
-
     std::function<rational (unsigned)>& var2val() { return m_var2val; } // setter
     const std::function<rational (unsigned)>& var2val() const { return m_var2val; } // getter
 

src/math/grobner/pdd_simplifier.h

@@ -27,7 +27,6 @@ class simplifier {
 public:
 
     simplifier(solver& s): s(s) {}
-    ~simplifier() {}
 
     void operator()();
 

src/math/lp/gomory.h

@@ -32,7 +32,6 @@ namespace lp {
         lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
     public:
         gomory(int_solver& lia);
-        ~gomory() {}
         lia_move operator()();
     };
 }

src/math/lp/int_branch.h

@@ -32,7 +32,6 @@ namespace lp {
 
     public:
         int_branch(int_solver& lia);
-        ~int_branch() {}
         lia_move operator()();
     };
 }

src/math/lp/int_cube.h

@@ -35,7 +35,6 @@ namespace lp {
         impq get_cube_delta_for_term(const lar_term& t) const;
     public:
         int_cube(int_solver& lia);
-        ~int_cube() {}
         lia_move operator()();
     };
 }

src/math/lp/int_gcd_test.h

@@ -47,7 +47,6 @@ namespace lp {
         void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
     public:
         int_gcd_test(int_solver& lia);
-        ~int_gcd_test() {}
         lia_move operator()();
         bool should_apply();
     };

src/math/lp/nex.h

@@ -54,7 +54,6 @@ class nex {
     virtual unsigned size() const { return 1; }
     virtual expr_type type() const = 0;
     virtual std::ostream& print(std::ostream&) const = 0;    
-    nex() {}
     bool is_elementary() const {
         switch(type()) {
         case expr_type::SUM:

src/math/simplex/bit_matrix.h

@@ -92,8 +92,6 @@ class bit_matrix {
         bool operator!=(row_iterator const& other) const { return m_index != other.m_index; }  
     };
 
-    bit_matrix() {}
-    ~bit_matrix() {}
     void reset(unsigned num_columns);
 
     row_iterator begin() { return row_iterator(*this, true); }

src/math/subpaving/subpaving_types.h

@@ -31,7 +31,7 @@ class exception {
 
 class power : public std::pair<var, unsigned> {
 public:
-    power():std::pair<var, unsigned>() {}
+    power() = default;
     power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
     var x() const { return first; }
     var get_var() const { return first; }

src/muz/base/dl_rule.h

@@ -313,7 +313,6 @@ namespace datalog {
         static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }
 
         rule() : m_ref_cnt(0), m_name(symbol::null) {}
-        ~rule() {}
 
         void deallocate(ast_manager & m);
 

src/muz/rel/dl_base.h

@@ -178,7 +178,7 @@ namespace datalog {
 
         class base_fn {
         public:
-            base_fn() {}
+            base_fn() = default;
             virtual ~base_fn() {}
         private:
             //private and undefined copy constructor and operator= to avoid copying
@@ -219,8 +219,6 @@ namespace datalog {
         */
         class mutator_fn : public base_fn {
         public:
-            ~mutator_fn() override {}
-
             virtual void operator()(base_object & t) = 0;
 
             virtual bool supports_attachment(base_object& other) { return false; }

src/muz/rel/dl_bound_relation.h

@@ -94,7 +94,6 @@ namespace datalog {
     struct uint_set2 {
         uint_set lt;
         uint_set le;
-        uint_set2() {}
         bool operator==(const uint_set2& other) const {
             return other.lt == lt && other.le == le;
         }

src/muz/spacer/spacer_context.h

@@ -235,7 +235,6 @@ class pred_transformer {
     public:
         frames (pred_transformer &pt) : m_pt (pt),
                                         m_size(0), m_sorted (true) {}
-        ~frames() {}
         void simplify_formulas ();
 
         pred_transformer& pt() const {return m_pt;}
@@ -356,7 +355,6 @@ class pred_transformer {
         rule2ptrule m_rules;
         tag2ptrule m_tags;
     public:
-        pt_rules() {}
         ~pt_rules() {for (auto &kv : m_rules) {dealloc(kv.m_value);}}
 
         bool find_by_rule(const datalog::rule &r, pt_rule* &ptr) {
@@ -439,7 +437,6 @@ class pred_transformer {
 
 public:
     pred_transformer(context& ctx, manager& pm, func_decl* head);
-    ~pred_transformer() {}
 
     inline bool use_native_mbp ();
     bool mk_mdl_rf_consistent(const datalog::rule *r, model &mdl);
@@ -825,7 +822,6 @@ class pob_queue {
 
 public:
     pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {}
-    ~pob_queue() {}
 
     void reset();
     pob* top();

src/parsers/smt2/smt2scanner.h

@@ -75,9 +75,7 @@ namespace smt2 {
             EOF_TOKEN
         };
 
-        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
-
-        ~scanner() {}    
+        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);  
 
         int get_line() const { return m_line; }
         int get_pos() const { return m_pos; }

src/parsers/util/scanner.h

@@ -39,8 +39,6 @@ class scanner {
 
     scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token=false);
 
-    ~scanner() {}    
-
     int get_line() const { return m_line; }
 
     int get_pos() const { return m_pos; }
@@ -86,5 +84,3 @@ class scanner {
     token read_bv_literal();
     bool state_ok();
 };
-
-

src/sat/dimacs.h

@@ -63,7 +63,6 @@ namespace dimacs {
         unsigned        m_node_id{ 0 };
         std::string     m_name;
         unsigned_vector m_args;
-        drat_record() {}
     };
 
     struct drat_pp {
@@ -111,6 +110,3 @@ namespace dimacs {
 
     };
 };
-
-
-

src/sat/sat_aig_finder.h

@@ -52,7 +52,6 @@ namespace sat {
 
     public:
         aig_finder(solver& s);
-        ~aig_finder() {}                
         void set(std::function<void (literal head, literal_vector const& ands)> const& f) { m_on_aig = f; }
         void set(std::function<void (literal head, literal cond, literal th, literal el)> const& f) { m_on_if = f; }
         void operator()(clause_vector& clauses);

src/sat/sat_anf_simplifier.h

@@ -111,7 +111,6 @@ namespace sat {
 
     public:
         anf_simplifier(solver& s) : s(s), m_eval_ts(0) {}
-        ~anf_simplifier() {}
 
         void operator()();
         void set(config const& cfg) { m_config = cfg; }

src/sat/sat_binspr.h

@@ -97,8 +97,6 @@ namespace sat {
             memset(m_false, 0, sizeof(unsigned) * max_lits);
         }
 
-        ~binspr() {}
-
         void operator()();
 
         void updt_params(params_ref const& p) {}