mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

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

Browse source 
* 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>
This commit is contained in:
Copilot 2026-02-01 16:51:26 -08:00 • committed by Nikolaj Bjorner
parent a01a624fa3
commit 17c8958d70
24 changed files with 82 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/dd/dd_bdd.h
View file

@ -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; }

24
src/math/dd/dd_pdd.h
View file

@ -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; }