Remove redundant default constructors when they're the only constructor (#8461)

* Initial plan

* Modernize C++ constructors to use C++11 default member initialization - Phase 1

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix theory_pb.h struct definition - move reset() back inside struct

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 2

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix opt_solver.h - revert rational initialization (complex type)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 3

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix sparse_matrix.h - explicitly initialize union member in default constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Remove unnecessary default constructors when they're the only constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

src/ast/ast.h

@@ -315,11 +315,11 @@ class sort_size {
         // of elements is at least bigger than 2^64.
         SS_FINITE_VERY_BIG,
         SS_INFINITE
-    } m_kind;
+    } m_kind = SS_INFINITE;
-    uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE
+    uint64_t m_size = 0; // It is only meaningful if m_kind == SS_FINITE
     sort_size(kind_t k, uint64_t r):m_kind(k), m_size(r) {}
 public:
-    sort_size():m_kind(SS_INFINITE), m_size(0) {}
+    sort_size() = default;
     sort_size(uint64_t sz):m_kind(SS_FINITE), m_size(sz) {}
     explicit sort_size(rational const& r) {
         if (r.is_uint64()) {

src/ast/converters/converter.h

@@ -23,9 +23,9 @@ Notes:
 #include "ast/ast_translation.h"
 
 class converter {
-    unsigned m_ref_count;
+    unsigned m_ref_count = 0;
 public:
-    converter():m_ref_count(0) {}
+    converter() = default;
     virtual ~converter() = default;
 
     void inc_ref() { ++m_ref_count;  }

src/ast/expr_delta_pair.h

@@ -22,10 +22,10 @@ Revision History:
    \brief Auxiliary structure used to cache the intermediate results of the variable substitution procedure.
 */
 struct expr_delta_pair {
-    expr *    m_node;
+    expr *    m_node = nullptr;
-    unsigned  m_delta;
+    unsigned  m_delta = 0;
     
-    expr_delta_pair():m_node(nullptr), m_delta(0) {}
+    expr_delta_pair() = default;
     expr_delta_pair(expr * n, unsigned d):m_node(n), m_delta(d) {}
     unsigned hash() const { return hash_u_u(m_node->hash(), m_delta); }
     bool operator==(const expr_delta_pair & e) const { return m_node == e.m_node && m_delta == e.m_delta; }

src/ast/expr_stat.h

@@ -24,12 +24,11 @@ Revision History:
 class expr;
 
 struct expr_stat {
-    unsigned m_sym_count; // symbol count
+    unsigned m_sym_count = 0; // symbol count
-    unsigned m_depth;     // depth
+    unsigned m_depth = 0;     // depth
-    unsigned m_const_count; // constant count
+    unsigned m_const_count = 0; // constant count
-    unsigned m_max_var_idx;  
+    unsigned m_max_var_idx = 0;  
-    bool     m_ground;
+    bool     m_ground = true;
-    expr_stat():m_sym_count(0), m_depth(0), m_const_count(0), m_max_var_idx(0), m_ground(true) {}
 };
 
 /**

src/ast/substitution/expr_offset.h

@@ -26,10 +26,10 @@ Revision History:
 #include "ast/ast.h"
 
 class expr_offset {
-    expr *    m_expr;
+    expr *    m_expr = nullptr;
-    unsigned  m_offset;
+    unsigned  m_offset = 0;
 public:
-    expr_offset():m_expr(nullptr), m_offset(0) {}
+    expr_offset() = default;
     expr_offset(expr * e, unsigned o):m_expr(e), m_offset(o) {}
     
     expr * get_expr() const { return m_expr; }

src/ast/substitution/expr_offset_map.h

@@ -28,8 +28,7 @@ template<typename T>
 class expr_offset_map {
     struct data {
         T        m_data;
-        unsigned m_timestamp;
+        unsigned m_timestamp = 0;
-        data():m_timestamp(0) {}
     };
     vector<svector<data> > m_map;
     unsigned               m_timestamp;

src/ast/substitution/var_offset_map.h

@@ -29,8 +29,7 @@ class var_offset_map {
 protected:
     struct data {
         T        m_data;
-        unsigned m_timestamp;
+        unsigned m_timestamp = 0;
-        data():m_timestamp(0) {}
     };
     
     svector<data>           m_map;

src/cmd_context/cmd_context.h

@@ -156,10 +156,10 @@ public:
 };
 
 struct builtin_decl {
-    family_id      m_fid;
+    family_id      m_fid = null_family_id;
-    decl_kind      m_decl;
+    decl_kind      m_decl = 0;
-    builtin_decl * m_next;
+    builtin_decl * m_next = nullptr;
-    builtin_decl():m_fid(null_family_id), m_decl(0), m_next(nullptr) {}
+    builtin_decl() = default;
     builtin_decl(family_id fid, decl_kind k, builtin_decl * n = nullptr):m_fid(fid), m_decl(k), m_next(n) {}
 };
 

src/math/dd/dd_bdd.h

@@ -57,12 +57,12 @@ namespace dd {
                 m_hi(hi),
                 m_index(0)
             {}
-            bdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {}
+            bdd_node() = default;
-            unsigned m_refcount : 10;
+            unsigned m_refcount : 10 = 0;
-            unsigned m_level : 22;
+            unsigned m_level : 22 = 0;
-            BDD      m_lo;
+            BDD      m_lo = 0;
-            BDD      m_hi;
+            BDD      m_hi = 0;
-            unsigned m_index;
+            unsigned m_index = 0;
             unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); }
             bool is_internal() const { return m_lo == 0 && m_hi == 0; }
             void set_internal() { m_lo = 0; m_hi = 0; }

src/math/dd/dd_pdd.h

@@ -93,12 +93,12 @@ namespace dd {
                 m_index(0)
             {}
 
-            node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {}
+            node() = default;
-            unsigned m_refcount : 10;
+            unsigned m_refcount : 10 = 0;
-            unsigned m_level : 22;
+            unsigned m_level : 22 = 0;
-            PDD      m_lo;
+            PDD      m_lo = 0;
-            PDD      m_hi;
+            PDD      m_hi = 0;
-            unsigned m_index;
+            unsigned m_index = 0;
             unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } 
             bool is_val() const { return m_hi == 0 && (m_lo != 0 || m_index == 0); }
             bool is_internal() const { return m_hi == 0 && m_lo == 0 && m_index != 0; }
@@ -160,13 +160,13 @@ namespace dd {
                 m_rest(UINT_MAX)
             {}
 
-            factor_entry(): m_p(0), m_v(0), m_degree(0), m_lc(UINT_MAX), m_rest(UINT_MAX) {}
+            factor_entry() = default;
 
-            PDD m_p;            // input
+            PDD m_p = 0;            // input
-            unsigned m_v;       // input
+            unsigned m_v = 0;       // input
-            unsigned m_degree;  // input
+            unsigned m_degree = 0;  // input
-            PDD m_lc;           // output
+            PDD m_lc = UINT_MAX;           // output
-            PDD m_rest;         // output
+            PDD m_rest = UINT_MAX;         // output
 
             bool is_valid() { return m_lc != UINT_MAX; }
 

src/math/lp/var_eqs.h

@@ -68,7 +68,7 @@ class var_eqs {
         stats() { memset(this, 0, sizeof(*this)); }
     };
 
-    T*                                m_merge_handler;    
+    T*                                m_merge_handler = nullptr;    
     union_find<var_eqs>               m_uf;
     lp::incremental_vector<std::pair<signed_var, signed_var>> m_trail;
     vector<svector<eq_edge>>          m_eqs;    // signed_var.index() -> the edges adjacent to signed_var.index()
@@ -81,7 +81,7 @@ class var_eqs {
         
     mutable stats m_stats;
 public:    
-    var_eqs(): m_merge_handler(nullptr), m_uf(*this) {}    
+    var_eqs(): m_uf(*this) {}    
     /**
        \brief push a scope    */
     void push() {

src/math/simplex/sparse_matrix.h

@@ -74,13 +74,13 @@ namespace simplex {
            with the column entry.
         */
         struct col_entry {
-            int m_row_id;
+            int m_row_id = 0;
             union {
                 int m_row_idx;
                 int m_next_free_col_entry_idx;
             };
             col_entry(int r, int i): m_row_id(r), m_row_idx(i) {}
-            col_entry(): m_row_id(0), m_row_idx(0) {}            
+            col_entry(): m_row_idx(0) {}            
             bool is_dead() const { return (unsigned) m_row_id == dead_id; }
         };
      
@@ -115,11 +115,10 @@ namespace simplex {
         */
         struct column {
             svector<col_entry> m_entries;
-            unsigned           m_size; 
+            unsigned           m_size = 0; 
-            int                m_first_free_idx;
+            int                m_first_free_idx = -1;
-            mutable unsigned   m_refs;
+            mutable unsigned   m_refs = 0;
             
-            column():m_size(0), m_first_free_idx(-1), m_refs(0) {}
             unsigned size() const { return m_size; }
             unsigned num_entries() const { return m_entries.size(); }
             void reset();

src/model/model2expr.h

@@ -29,10 +29,9 @@ typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
 
 class mk_fresh_name {
     symbol_set m_symbols;
-    char       m_char;
+    char       m_char = 'A';
-    unsigned   m_num;
+    unsigned   m_num = 0;
 public:
-    mk_fresh_name(): m_char('A'), m_num(0) {}
     void add(ast* a);
     void add(symbol const& s) { m_symbols.insert(s); }
     symbol next();

src/sat/sat_lookahead.h

@@ -116,15 +116,13 @@ namespace sat {
         };
 
         struct prefix {
-            unsigned m_prefix;
+            unsigned m_prefix = 0;
-            unsigned m_length;
+            unsigned m_length = 0;
-            prefix(): m_prefix(0), m_length(0) {}            
         };
 
         struct lit_info {
-            double     m_lookahead_reward;
+            double     m_lookahead_reward = 0;
-            unsigned  m_double_lookahead;
+            unsigned  m_double_lookahead = 0;
-            lit_info(): m_lookahead_reward(0), m_double_lookahead(0) {}
         };
 
         struct stats {

src/sat/smt/euf_ackerman.h

@@ -29,10 +29,10 @@ namespace euf {
     class ackerman {
 
         struct inference : dll_base<inference>{
-            expr* a, *b, *c;
+            expr* a = nullptr, *b = nullptr, *c = nullptr;
             unsigned   m_count{ 0 };
-            bool is_cc;
+            bool is_cc = false;
-            inference(): a(nullptr), b(nullptr), c(nullptr), is_cc(false) {}
+            inference() = default;
             inference(app* a, app* b): a(a), b(b), c(nullptr), is_cc(true) {}
             inference(expr* a, expr* b, expr* c): a(a), b(b), c(c), is_cc(false) {}
         };

src/sat/smt/sat_smt.h

@@ -30,14 +30,13 @@ namespace sat {
     };
 
     class constraint_base {
-        extension* m_ex;
+        extension* m_ex = nullptr;
         unsigned   m_mem[0];
         static size_t ext_size() {
             return sizeof(((constraint_base*)nullptr)->m_ex);
         }
 
     public:
-        constraint_base(): m_ex(nullptr) {}
         void*  mem() { return m_mem; }
 
         static size_t obj_size(size_t sz) { 

src/smt/theory_arith.h

@@ -111,13 +111,13 @@ namespace smt {
         */
         struct row_entry {
             numeral     m_coeff;
-            theory_var  m_var;
+            theory_var  m_var = 0;
             union {
                 int       m_col_idx;
                 int       m_next_free_row_entry_idx;
             };
             
-            row_entry():m_var(0), m_col_idx(0) {}
+            row_entry(): m_col_idx(0) {}
             row_entry(numeral const & c, theory_var v): m_coeff(c), m_var(v), m_col_idx(0) {}
             bool is_dead() const { return m_var == null_theory_var; }
         };
@@ -128,14 +128,14 @@ namespace smt {
            with the column entry.
         */
         struct col_entry {
-            int m_row_id;
+            int m_row_id = 0;
             union {
                 int m_row_idx;
                 int m_next_free_row_entry_idx;
             };
             
             col_entry(int r, int i): m_row_id(r), m_row_idx(i) {}
-            col_entry(): m_row_id(0), m_row_idx(0) {}
+            col_entry(): m_row_idx(0) {}
             bool is_dead() const { return m_row_id == dead_row_id; }
         };
      
@@ -189,10 +189,9 @@ namespace smt {
         */
         struct column {
             svector<col_entry> m_entries;
-            unsigned           m_size; 
+            unsigned           m_size = 0; 
-            int                m_first_free_idx;
+            int                m_first_free_idx = -1;
             
-            column():m_size(0), m_first_free_idx(-1) {}
             unsigned size() const { return m_size; }
             unsigned num_entries() const { return m_entries.size(); }
             void reset();
@@ -236,7 +235,7 @@ namespace smt {
             vector<numeral>   m_lit_coeffs;
             vector<numeral>   m_eq_coeffs;
             vector<parameter> m_params;
-            bool m_init;
+            bool m_init = false;
 
             bool empty() const { 
                 return m_eq_coeffs.empty() && m_lit_coeffs.empty(); 
@@ -245,7 +244,6 @@ namespace smt {
             void init();
 
         public:
-            antecedents_t(): m_init(false) {}
             void reset();
             literal_vector const& lits() const { return m_lits; }
             eq_vector const& eqs() const { return m_eqs; }

src/smt/theory_bv.h

@@ -54,8 +54,7 @@ namespace smt {
         };
 
         struct bit_atom : public atom {
-            var_pos_occ * m_occs;
+            var_pos_occ * m_occs = nullptr;
-            bit_atom():m_occs(nullptr) {}
             bool is_bit() const override { return true; }
         };
 

src/smt/theory_pb.h

@@ -244,19 +244,11 @@ namespace smt {
 
 
         struct var_info {
-            ineq_watch*  m_lit_watch[2];
+            ineq_watch*  m_lit_watch[2] = { nullptr, nullptr };
-            ineq*        m_ineq;
+            ineq*        m_ineq = nullptr;
 
-            card_watch*  m_lit_cwatch[2];
+            card_watch*  m_lit_cwatch[2] = { nullptr, nullptr };
-            card*        m_card;
+            card*        m_card = nullptr;
-            
-            var_info(): m_ineq(nullptr), m_card(nullptr)
-            {
-                m_lit_watch[0] = nullptr;
-                m_lit_watch[1] = nullptr;
-                m_lit_cwatch[0] = nullptr;
-                m_lit_cwatch[1] = nullptr;
-            }
 
             void reset() {
                 dealloc(m_lit_watch[0]);

src/util/approx_nat.h

@@ -23,10 +23,10 @@ Notes:
 #include<climits>
 
 class approx_nat {
-    unsigned m_value;
+    unsigned m_value = 0;
     static const unsigned m_limit = UINT_MAX >> 2;
 public:
-    approx_nat():m_value(0) {}
+    approx_nat() = default;
     explicit approx_nat(unsigned val);
     bool is_huge() const { return m_value == UINT_MAX; }
     unsigned get_value() const { return m_value; }

src/util/checked_int64.h

@@ -34,14 +34,14 @@ class overflow_exception : public z3_exception {
 
 template<bool CHECK>
 class checked_int64 {
-    int64_t m_value;
+    int64_t m_value = 0;
     typedef checked_int64 ci;
     
     rational r64(int64_t i) const { return rational(i, rational::i64()); }
 
 public:
 
-    checked_int64(): m_value(0) {}
+    checked_int64() = default;
     checked_int64(int64_t v): m_value(v) {}
 
     bool is_zero() const { return m_value == 0; }

src/util/ema.h

@@ -21,11 +21,11 @@ Revision History:
 #pragma once
 
 class ema {
-    double m_alpha, m_beta, m_value;
+    double m_alpha = 0, m_beta = 1, m_value = 0;
-    unsigned m_period, m_wait;
+    unsigned m_period = 0, m_wait = 0;
     bool invariant() const { return 0 <= m_alpha && m_alpha <= m_beta && m_beta <= 1 && m_wait <= m_period; }
  public:
-    ema(): m_alpha(0), m_beta(1), m_value(0), m_period(0), m_wait(0) {
+    ema() {
         SASSERT(invariant());
     }
 

src/util/inf_s_integer.h

@@ -25,8 +25,8 @@ class inf_s_integer {
     static inf_s_integer m_zero;
     static inf_s_integer m_one;
     static inf_s_integer m_minus_one;
-    int m_first;
+    int m_first = 0;
-    int m_second;
+    int m_second = 0;
  public:
 
     unsigned hash() const { 
@@ -44,7 +44,7 @@ class inf_s_integer {
 
     std::string to_string() const;
 
-    inf_s_integer():m_first(0), m_second(0) {}
+    inf_s_integer() = default;
 
     explicit inf_s_integer(int n):m_first(n), m_second(0) {}
     explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); }

src/util/mpbq.h

@@ -31,11 +31,11 @@ Revision History:
 #include "util/vector.h"
 
 class mpbq {
-    mpz      m_num;
+    mpz      m_num = 0;
-    unsigned m_k;    // we don't need mpz here. 2^(2^32-1) is a huge number, we will not even be able to convert the mpbq into an mpq
+    unsigned m_k = 0;    // we don't need mpz here. 2^(2^32-1) is a huge number, we will not even be able to convert the mpbq into an mpq
     friend class mpbq_manager;
 public:
-    mpbq():m_num(0), m_k(0) {}
+    mpbq() = default;
     mpbq(int v):m_num(v), m_k(0) {}
     mpbq(int v, unsigned k):m_num(v), m_k(k) {}
     mpz const & numerator() const { return m_num; }