From a62fede64ba641cb6158f3bfdd22fd86f87d55f9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 23 Sep 2024 08:17:58 +0100 Subject: [PATCH] remove a few default constructors --- src/ast/recfun_decl_plugin.cpp | 2 -- src/ast/seq_decl_plugin.h | 2 +- src/ast/sls/sls_valuation.h | 2 +- src/math/grobner/grobner.h | 4 ++-- src/math/lp/explanation.h | 2 +- src/math/lp/general_matrix.h | 2 +- src/math/lp/hnf_cutter.cpp | 3 +-- src/math/lp/implied_bound.h | 2 +- src/math/lp/indexed_vector.h | 2 +- src/math/lp/lar_term.h | 2 +- src/math/lp/nla_tangent_lemmas.h | 2 +- src/muz/base/dl_util.h | 1 - src/muz/spacer/spacer_unsat_core_plugin.h | 2 +- src/smt/fingerprints.h | 2 +- src/tactic/aig/aig.cpp | 1 - src/util/mpq.h | 6 +++--- 16 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 37e5d359ea4..a976ee3c9c8 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -170,8 +170,6 @@ namespace recfun { vector m_branches; public: - case_state() : m_reg(), m_branches() {} - bool empty() const { return m_branches.empty(); } branch pop_branch() { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c6550d33aad..c08ed6f7a5e 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -446,7 +446,7 @@ class seq_util { /* Default constructor of invalid info. */ - info() {} + info() = default; /* Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value. diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 66d7e0281cc..f10fd8f0bfc 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -33,7 +33,7 @@ namespace bv { unsigned nw = 0; unsigned mask = 0; - bvect() {} + bvect() = default; bvect(unsigned sz) : svector(sz, (unsigned)0) {} void set_bw(unsigned bw); diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h index 6adffea7cc5..83c0d8a5e83 100644 --- a/src/math/grobner/grobner.h +++ b/src/math/grobner/grobner.h @@ -48,7 +48,7 @@ class grobner { friend class grobner; friend struct monomial_lt; - monomial() {} + monomial() = default; public: rational const & get_coeff() const { return m_coeff; } unsigned get_degree() const { return m_vars.size(); } @@ -63,7 +63,7 @@ class grobner { ptr_vector m_monomials; //!< sorted monomials v_dependency * m_dep; //!< justification for the equality friend class grobner; - equation() {} + equation() = default; public: unsigned get_num_monomials() const { return m_monomials.size(); } monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; } diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index 960c5fb4ab5..9d8099c1e9c 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -29,7 +29,7 @@ class explanation { vector> m_vector; ci_set m_set; public: - explanation() {} + explanation() = default; template explanation(const T& t) { diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index fb1030e6b10..e42f01ad72c 100644 --- a/src/math/lp/general_matrix.h +++ b/src/math/lp/general_matrix.h @@ -180,7 +180,7 @@ class general_matrix { m_column_permutation.transpose_from_left(j, k); } - general_matrix(){} + general_matrix() = default; general_matrix(unsigned n) : m_row_permutation(n), m_column_permutation(n), diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index b120b7aac0e..7f1af2aaa67 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -19,8 +19,7 @@ namespace lp { lia(lia), lra(lia.lra), m_settings(lia.settings()), - m_abs_max(zero_of_type()), - m_var_register() {} + m_abs_max(zero_of_type()) {} bool hnf_cutter::is_full() const { return diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h index 195ec03599d..6d7fc54b9d1 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -44,7 +44,7 @@ class implied_bound { k = static_cast(k / 2); return k; } - implied_bound(){} + implied_bound() = default; implied_bound(const mpq & a, unsigned j, bool is_lower_bound, diff --git a/src/math/lp/indexed_vector.h b/src/math/lp/indexed_vector.h index 9f3119e9a16..5740fdc217a 100644 --- a/src/math/lp/indexed_vector.h +++ b/src/math/lp/indexed_vector.h @@ -76,7 +76,7 @@ class indexed_vector { } - indexed_vector() {} + indexed_vector() = default; void resize(unsigned data_size); unsigned data_size() const { diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 6547377d365..87a0c282a37 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -70,7 +70,7 @@ class lar_term { } } // constructors - lar_term() {} + lar_term() = default; lar_term(const vector>& coeffs) { for (auto const& p : coeffs) { add_monomial(p.first, p.second); diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h index 1895b3fcba6..daa45a41aec 100644 --- a/src/math/lp/nla_tangent_lemmas.h +++ b/src/math/lp/nla_tangent_lemmas.h @@ -17,7 +17,7 @@ struct point { rational x; rational y; point(const rational& a, const rational& b): x(a), y(b) {} - point() {} + point() = default; inline point& operator*=(rational a) { x *= a; y *= a; diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 401d8e81670..ac1bed51e67 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -347,7 +347,6 @@ namespace datalog { class rule_counter : public var_counter { public: - rule_counter(){} void count_rule_vars(const rule * r, int coef = 1); unsigned get_max_rule_var(const rule& r); }; diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index a7ea4c89bb6..b844cdd469a 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/src/muz/spacer/spacer_unsat_core_plugin.h @@ -33,7 +33,7 @@ namespace spacer { unsat_core_plugin(unsat_core_learner& learner); virtual ~unsat_core_plugin() = default; virtual void compute_partial_core(proof* step) = 0; - virtual void finalize(){}; + virtual void finalize(){} unsat_core_learner& m_ctx; }; diff --git a/src/smt/fingerprints.h b/src/smt/fingerprints.h index a602f25cd65..6a0bc1ccd2a 100644 --- a/src/smt/fingerprints.h +++ b/src/smt/fingerprints.h @@ -32,7 +32,7 @@ namespace smt { enode** m_args = nullptr; friend class fingerprint_set; - fingerprint() {} + fingerprint() = default; public: fingerprint(region & r, void * d, unsigned d_hash, expr* def, unsigned n, enode * const * args); void * get_data() const { return m_data; } diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 433120b48b6..e599829694a 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -50,7 +50,6 @@ struct aig { unsigned m_ref_count; aig_lit m_children[2]; unsigned m_mark:1; - aig() {} }; #if Z3DEBUG diff --git a/src/util/mpq.h b/src/util/mpq.h index 286c2758d86..87ee5e17da4 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -23,12 +23,12 @@ Revision History: class mpq { mpz m_num; - mpz m_den; + mpz m_den = 1; friend class mpq_manager; friend class mpq_manager; public: - mpq(int v):m_num(v), m_den(1) {} - mpq():m_den(1) {} + mpq(int v) : m_num(v) {} + mpq() = default; mpq(mpq &&) noexcept = default; mpq & operator=(mpq&&) = default; mpq & operator=(mpq const&) = delete;