From 23c531a4c1233f9ecbdbfdb88c05601c3e9badcf Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Feb 2026 16:51:26 -0800 Subject: [PATCH] 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 | 6 +++--- src/ast/converters/converter.h | 4 ++-- src/ast/expr_delta_pair.h | 6 +++--- src/ast/expr_stat.h | 11 +++++------ src/ast/substitution/expr_offset.h | 6 +++--- src/ast/substitution/expr_offset_map.h | 3 +-- src/ast/substitution/var_offset_map.h | 3 +-- src/cmd_context/cmd_context.h | 8 ++++---- src/math/dd/dd_bdd.h | 12 ++++++------ src/math/dd/dd_pdd.h | 24 ++++++++++++------------ src/math/lp/var_eqs.h | 4 ++-- src/math/simplex/sparse_matrix.h | 11 +++++------ src/model/model2expr.h | 5 ++--- src/sat/sat_lookahead.h | 10 ++++------ src/sat/smt/euf_ackerman.h | 6 +++--- src/sat/smt/sat_smt.h | 3 +-- src/smt/theory_arith.h | 16 +++++++--------- src/smt/theory_bv.h | 3 +-- src/smt/theory_pb.h | 16 ++++------------ src/util/approx_nat.h | 4 ++-- src/util/checked_int64.h | 4 ++-- src/util/ema.h | 6 +++--- src/util/inf_s_integer.h | 6 +++--- src/util/mpbq.h | 6 +++--- 24 files changed, 82 insertions(+), 101 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index da3d7a4ee..779913f17 100644 --- a/src/ast/ast.h +++ b/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; - uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE + } m_kind = SS_INFINITE; + 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()) { diff --git a/src/ast/converters/converter.h b/src/ast/converters/converter.h index 3e572855b..05ba1eb08 100644 --- a/src/ast/converters/converter.h +++ b/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; } diff --git a/src/ast/expr_delta_pair.h b/src/ast/expr_delta_pair.h index e07590db6..df5c8d74f 100644 --- a/src/ast/expr_delta_pair.h +++ b/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; - unsigned m_delta; + expr * m_node = nullptr; + 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; } diff --git a/src/ast/expr_stat.h b/src/ast/expr_stat.h index 6bfedef2c..932b497b3 100644 --- a/src/ast/expr_stat.h +++ b/src/ast/expr_stat.h @@ -24,12 +24,11 @@ Revision History: class expr; struct expr_stat { - unsigned m_sym_count; // symbol count - unsigned m_depth; // depth - unsigned m_const_count; // constant count - unsigned m_max_var_idx; - bool m_ground; - expr_stat():m_sym_count(0), m_depth(0), m_const_count(0), m_max_var_idx(0), m_ground(true) {} + unsigned m_sym_count = 0; // symbol count + unsigned m_depth = 0; // depth + unsigned m_const_count = 0; // constant count + unsigned m_max_var_idx = 0; + bool m_ground = true; }; /** diff --git a/src/ast/substitution/expr_offset.h b/src/ast/substitution/expr_offset.h index 1e3b9e11d..d52182117 100644 --- a/src/ast/substitution/expr_offset.h +++ b/src/ast/substitution/expr_offset.h @@ -26,10 +26,10 @@ Revision History: #include "ast/ast.h" class expr_offset { - expr * m_expr; - unsigned m_offset; + expr * m_expr = nullptr; + 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; } diff --git a/src/ast/substitution/expr_offset_map.h b/src/ast/substitution/expr_offset_map.h index f2f5406d7..c4249648f 100644 --- a/src/ast/substitution/expr_offset_map.h +++ b/src/ast/substitution/expr_offset_map.h @@ -28,8 +28,7 @@ template class expr_offset_map { struct data { T m_data; - unsigned m_timestamp; - data():m_timestamp(0) {} + unsigned m_timestamp = 0; }; vector > m_map; unsigned m_timestamp; diff --git a/src/ast/substitution/var_offset_map.h b/src/ast/substitution/var_offset_map.h index 288ddc867..64dff9c14 100644 --- a/src/ast/substitution/var_offset_map.h +++ b/src/ast/substitution/var_offset_map.h @@ -29,8 +29,7 @@ class var_offset_map { protected: struct data { T m_data; - unsigned m_timestamp; - data():m_timestamp(0) {} + unsigned m_timestamp = 0; }; svector m_map; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8a742824b..611b1c207 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -156,10 +156,10 @@ public: }; struct builtin_decl { - family_id m_fid; - decl_kind m_decl; - builtin_decl * m_next; - builtin_decl():m_fid(null_family_id), m_decl(0), m_next(nullptr) {} + family_id m_fid = null_family_id; + decl_kind m_decl = 0; + builtin_decl * 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) {} }; diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h index 109f3dc19..93332bd91 100644 --- a/src/math/dd/dd_bdd.h +++ b/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) {} - unsigned m_refcount : 10; - unsigned m_level : 22; - BDD m_lo; - BDD m_hi; - unsigned m_index; + bdd_node() = default; + unsigned m_refcount : 10 = 0; + unsigned m_level : 22 = 0; + BDD m_lo = 0; + BDD m_hi = 0; + 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; } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index b96e5f04b..ecdaf1e69 100644 --- a/src/math/dd/dd_pdd.h +++ b/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) {} - unsigned m_refcount : 10; - unsigned m_level : 22; - PDD m_lo; - PDD m_hi; - unsigned m_index; + node() = default; + unsigned m_refcount : 10 = 0; + unsigned m_level : 22 = 0; + PDD m_lo = 0; + PDD m_hi = 0; + 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 - unsigned m_v; // input - unsigned m_degree; // input - PDD m_lc; // output - PDD m_rest; // output + PDD m_p = 0; // input + unsigned m_v = 0; // input + unsigned m_degree = 0; // input + PDD m_lc = UINT_MAX; // output + PDD m_rest = UINT_MAX; // output bool is_valid() { return m_lc != UINT_MAX; } diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 48f5ec61a..599051160 100644 --- a/src/math/lp/var_eqs.h +++ b/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 m_uf; lp::incremental_vector> m_trail; vector> 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() { diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 0dfd1a2ad..942873b5f 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/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 m_entries; - unsigned m_size; - int m_first_free_idx; - mutable unsigned m_refs; + unsigned m_size = 0; + int m_first_free_idx = -1; + 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(); diff --git a/src/model/model2expr.h b/src/model/model2expr.h index 19299f456..f44cfaa29 100644 --- a/src/model/model2expr.h +++ b/src/model/model2expr.h @@ -29,10 +29,9 @@ typedef hashtable symbol_set; class mk_fresh_name { symbol_set m_symbols; - char m_char; - unsigned m_num; + char m_char = 'A'; + 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(); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 31192fa28..87757ba59 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -116,15 +116,13 @@ namespace sat { }; struct prefix { - unsigned m_prefix; - unsigned m_length; - prefix(): m_prefix(0), m_length(0) {} + unsigned m_prefix = 0; + unsigned m_length = 0; }; struct lit_info { - double m_lookahead_reward; - unsigned m_double_lookahead; - lit_info(): m_lookahead_reward(0), m_double_lookahead(0) {} + double m_lookahead_reward = 0; + unsigned m_double_lookahead = 0; }; struct stats { diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h index b5af2f689..846ddb8ae 100644 --- a/src/sat/smt/euf_ackerman.h +++ b/src/sat/smt/euf_ackerman.h @@ -29,10 +29,10 @@ namespace euf { class ackerman { struct inference : dll_base{ - expr* a, *b, *c; + expr* a = nullptr, *b = nullptr, *c = nullptr; unsigned m_count{ 0 }; - bool is_cc; - inference(): a(nullptr), b(nullptr), c(nullptr), is_cc(false) {} + bool 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) {} }; diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index b509f0a9e..c661288f5 100644 --- a/src/sat/smt/sat_smt.h +++ b/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) { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index f1ec345b1..13e7a0986 100644 --- a/src/smt/theory_arith.h +++ b/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 m_entries; - unsigned m_size; - int m_first_free_idx; + unsigned m_size = 0; + 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 m_lit_coeffs; vector m_eq_coeffs; vector 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; } diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 5ba10442d..476912117 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -54,8 +54,7 @@ namespace smt { }; struct bit_atom : public atom { - var_pos_occ * m_occs; - bit_atom():m_occs(nullptr) {} + var_pos_occ * m_occs = nullptr; bool is_bit() const override { return true; } }; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 96e1c96bd..73c9d5cba 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -244,19 +244,11 @@ namespace smt { struct var_info { - ineq_watch* m_lit_watch[2]; - ineq* m_ineq; + ineq_watch* m_lit_watch[2] = { nullptr, nullptr }; + ineq* m_ineq = nullptr; - card_watch* m_lit_cwatch[2]; - card* m_card; - - 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; - } + card_watch* m_lit_cwatch[2] = { nullptr, nullptr }; + card* m_card = nullptr; void reset() { dealloc(m_lit_watch[0]); diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h index 67e672f84..248021620 100644 --- a/src/util/approx_nat.h +++ b/src/util/approx_nat.h @@ -23,10 +23,10 @@ Notes: #include 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; } diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h index aab741682..14d716b0d 100644 --- a/src/util/checked_int64.h +++ b/src/util/checked_int64.h @@ -34,14 +34,14 @@ class overflow_exception : public z3_exception { template 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; } diff --git a/src/util/ema.h b/src/util/ema.h index 99491bc72..95bec7f05 100644 --- a/src/util/ema.h +++ b/src/util/ema.h @@ -21,11 +21,11 @@ Revision History: #pragma once class ema { - double m_alpha, m_beta, m_value; - unsigned m_period, m_wait; + double m_alpha = 0, m_beta = 1, m_value = 0; + 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()); } diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index a02ba70fd..873ad2bde 100644 --- a/src/util/inf_s_integer.h +++ b/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_second; + int m_first = 0; + 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); } diff --git a/src/util/mpbq.h b/src/util/mpbq.h index edd864dc3..1bb6c396e 100644 --- a/src/util/mpbq.h +++ b/src/util/mpbq.h @@ -31,11 +31,11 @@ Revision History: #include "util/vector.h" class mpbq { - mpz m_num; - 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 + mpz m_num = 0; + 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; }