delete more default constructors

reduces code size by 0.1%

Author: nunoplopes

src/ackermannization/ackr_bound_probe.cpp

@@ -60,8 +60,6 @@ class ackr_bound_probe : public probe {
     };
 
 public:
-    ackr_bound_probe() {}
-
     result operator()(goal const & g) override {
         proc p(g.m());
         unsigned sz = g.size();

src/ast/converters/model_converter.h

@@ -71,9 +71,6 @@ class model_converter : public converter {
     void display_del(std::ostream& out, func_decl* f) const;
     void display_add(std::ostream& out, ast_manager& m);
 public:
-
-    model_converter() {}
-
     void set_completion(bool f) { m_completion = f; }
 
     virtual void operator()(model_ref & m) = 0;

src/ast/recfun_decl_plugin.cpp

@@ -417,7 +417,6 @@ namespace recfun {
     }
 
     namespace decl {
-        plugin::plugin() : decl_plugin(), m_defs(), m_case_defs() {}
         plugin::~plugin() { finalize(); }
 
         void plugin::finalize() {

src/ast/recfun_decl_plugin.h

@@ -173,7 +173,6 @@ namespace recfun {
             void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
 
         public:
-            plugin();
             ~plugin() override;
             void finalize() override;
 

src/ast/rewriter/var_subst.h

@@ -94,7 +94,7 @@ class expr_free_vars {
     ptr_vector<sort> m_sorts;
     ptr_vector<expr> m_todo;
 public:
-    expr_free_vars() {}
+    expr_free_vars() = default;
     expr_free_vars(expr* e) { (*this)(e); }
     void reset();
     void operator()(expr* e);

src/ast/simplifiers/linear_equation.h

@@ -35,7 +35,7 @@ class linear_equation {
     mpz *      m_as;        // precise coefficients
     double *   m_approx_as; // approximated coefficients
     var *      m_xs;        // var ids
-    linear_equation() {}
+    linear_equation() = default;
 public:
     unsigned size() const { return m_size; }
     mpz const & a(unsigned idx) const { SASSERT(idx < m_size); return m_as[idx]; }

src/cmd_context/cmd_context.h

@@ -47,7 +47,7 @@ class func_decls {
     bool signatures_collide(func_decl* f, func_decl* g) const;
     bool signatures_collide(unsigned n, sort*const* domain, sort* range, func_decl* g) const;
 public:
-    func_decls() {}
+    func_decls() = default;
     func_decls(ast_manager & m, func_decl * f);
     void finalize(ast_manager & m);
     bool contains(func_decl * f) const;

src/math/interval/mod_interval.h

@@ -26,7 +26,7 @@ namespace bv {
         bool tight = true;
 
         interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
-        interval_tpl() {}
+        interval_tpl() = default;
 
         bool invariant() const {
             return 
@@ -167,7 +167,7 @@ namespace bv {
         iinterval i;
         rinterval r;
 
-        interval() {}
+        interval() = default;
 
         interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
             if (sz <= 64) {

src/math/lp/factorization.h

@@ -24,7 +24,7 @@ class factor {
     factor_type  m_type = factor_type::VAR;
     bool         m_sign = false;
 public:
-    factor() { }
+    factor() = default;
     explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {}
     unsigned var() const { return m_var; }
     factor_type type() const { return m_type; }

src/math/lp/indexed_value.h

@@ -29,7 +29,7 @@ class indexed_value {
     // m_other is the offset of the corresponding element in its vector : for a row element it points to the column element offset,
     // for a column element it points to the row element offset
     unsigned m_other;
-    indexed_value() {}
+    indexed_value() = default;
 
     indexed_value(T v, unsigned i, unsigned other) :
         m_value(v), m_index(i), m_other(other) {