From e844aef896be906d2f100f7e7f216c9878cd874b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Jun 2020 20:30:21 +0100 Subject: [PATCH] remove a few more copy constructors, though still not enough to enable the assertion in vector I give up for now; there are too many copies left for little return.. --- src/ast/justified_expr.h | 2 +- src/ast/recfun_decl_plugin.cpp | 2 -- src/math/dd/dd_pdd.h | 2 +- src/math/lp/indexed_value.h | 13 ------------- src/math/lp/numeric_pair.h | 2 -- src/math/simplex/model_based_opt.h | 1 - src/opt/maxsmt.h | 2 -- src/opt/pb_sls.cpp | 10 ---------- src/qe/qe_arrays.cpp | 11 +++-------- src/util/array_map.h | 16 ++++++++-------- src/util/inf_rational.h | 11 ++--------- src/util/inf_s_integer.h | 9 +-------- src/util/obj_ref.h | 7 ++----- src/util/ref_vector.h | 14 +++++++++++++- src/util/scoped_numeral.h | 6 ++---- src/util/scoped_numeral_vector.h | 15 ++++++++++----- src/util/uint_set.h | 16 +--------------- 17 files changed, 44 insertions(+), 95 deletions(-) diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index 2e49051e3..786061065 100644 --- a/src/ast/justified_expr.h +++ b/src/ast/justified_expr.h @@ -39,7 +39,7 @@ public: m.inc_ref(m_proof); } - justified_expr(justified_expr && other): + justified_expr(justified_expr && other) noexcept : m(other.m), m_fml(nullptr), m_proof(nullptr) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 99e0da198..87a09afb0 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -131,8 +131,6 @@ namespace recfun { path(nullptr), to_split(nullptr), to_unfold(to_unfold) {} branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : path(path), to_split(to_split), to_unfold(to_unfold) {} - branch(branch const & from) : - path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {} }; // state for computing cases from the RHS of a functions' definition diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index b24f95c6d..d12af2585 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -320,7 +320,7 @@ namespace dd { public: pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); } pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); } - pdd(pdd && other): root(0), m(other.m) { std::swap(root, other.root); } + pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } pdd& operator=(pdd const& other); ~pdd() { m.dec_ref(root); } pdd lo() const { return pdd(m.lo(root), m); } diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h index 38e48f4aa..c48376470 100644 --- a/src/math/lp/indexed_value.h +++ b/src/math/lp/indexed_value.h @@ -35,19 +35,6 @@ public: m_value(v), m_index(i), m_other(other) { } - indexed_value(const indexed_value & iv) { - m_value = iv.m_value; - m_index = iv.m_index; - m_other = iv.m_other; - } - - indexed_value & operator=(const indexed_value & right_side) { - m_value = right_side.m_value; - m_index = right_side.m_index; - m_other = right_side.m_other; - return *this; - } - const T & value() const { return m_value; } diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h index cd992ccb2..e7586cf5a 100644 --- a/src/math/lp/numeric_pair.h +++ b/src/math/lp/numeric_pair.h @@ -144,8 +144,6 @@ struct numeric_pair { explicit numeric_pair(const X & n) : x(n), y(0) { } - numeric_pair(const numeric_pair & n) : x(n.x), y(n.y) {} - template numeric_pair(X xp, Y yp) : x(convert_struct::convert(xp)), y(convert_struct::convert(yp)) {} diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index 7311850ab..4740a4899 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -67,7 +67,6 @@ namespace opt { struct def { def(): m_div(1) {} def(row const& r, unsigned x); - def(def const& other): m_vars(other.m_vars), m_coeff(other.m_coeff), m_div(other.m_div) {} vector m_vars; rational m_coeff; rational m_div; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 291ec26d8..02fc16e02 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -64,8 +64,6 @@ namespace opt { void set_value(lbool t) { value = t; } bool is_true() const { return value == l_true; } soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {} - soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {} - soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; } }; ast_manager& m; maxsat_context& m_c; diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index c433f56d3..315b6f22a 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -77,16 +77,6 @@ namespace smt { m_value(m), m_eq(true) {} - clause(clause const& cls): - m_lits(cls.m_lits), - m_weights(cls.m_weights.m()), - m_k(cls.m_k), - m_value(cls.m_value), - m_eq(cls.m_eq) { - for (unsigned i = 0; i < cls.m_weights.size(); ++i) { - m_weights.push_back(cls.m_weights[i]); - } - } }; struct stats { diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index cee6e3e8e..cec3a7726 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -899,12 +899,8 @@ namespace qe { expr_ref_vector idx; expr_ref_vector val; vector rval; - idx_val(expr_ref_vector & idx, expr_ref_vector & val, vector const& rval): idx(idx), val(val), rval(rval) {} - idx_val& operator=(idx_val const& o) { - idx.reset(); val.reset(); rval.reset(); - idx.append(o.idx); val.append(o.val); rval.append(o.rval); - return *this; - } + idx_val(expr_ref_vector && idx, expr_ref_vector && val, vector && rval): + idx(std::move(idx)), val(std::move(val)), rval(std::move(rval)) {} }; ast_manager& m; array_util m_arr_u; @@ -1049,8 +1045,7 @@ namespace qe { } if (is_new) { // new repr, val, and sel const - vector rvals = to_num(vals); - m_idxs.push_back(idx_val(idxs, vals, rvals)); + m_idxs.push_back(idx_val(std::move(idxs), std::move(vals), to_num(vals))); app_ref c (m.mk_fresh_const ("sel", val_sort), m); m_sel_consts.push_back (c); // substitute sel term with new const diff --git a/src/util/array_map.h b/src/util/array_map.h index f3f99d015..91d226dab 100644 --- a/src/util/array_map.h +++ b/src/util/array_map.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef ARRAY_MAP_H_ -#define ARRAY_MAP_H_ +#pragma once #include "util/vector.h" #include "util/optional.h" @@ -40,9 +39,9 @@ class array_map { entry(Key const & k, Data const & d, unsigned t): m_key(k), m_data(d), m_timestamp(t) {} }; - unsigned m_timestamp; - unsigned m_garbage; - unsigned m_non_garbage; + unsigned m_timestamp = 0; + unsigned m_garbage = 0; + unsigned m_non_garbage = 0; static const unsigned m_gc_threshold = 10000; vector, CallDestructors > m_map; Plugin m_plugin; @@ -76,7 +75,10 @@ class array_map { public: - array_map(Plugin const & p = Plugin()):m_timestamp(0), m_garbage(0), m_non_garbage(0), m_plugin(p) {} + array_map() = default; + array_map(array_map&&) noexcept = default; + array_map(Plugin const & p) : m_plugin(p) {} + ~array_map() { really_flush(); } bool contains(Key const & k) const { @@ -155,5 +157,3 @@ public: } }; - -#endif /* ARRAY_MAP_H_ */ diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index c3f4160ba..86e04543c 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -17,8 +17,8 @@ Author: Revision History: --*/ -#ifndef INF_RATIONAL_H_ -#define INF_RATIONAL_H_ +#pragma once + #include #include #include "util/debug.h" @@ -67,11 +67,6 @@ class inf_rational { inf_rational() {} - inf_rational(const inf_rational & r): - m_first(r.m_first), - m_second(r.m_second) - {} - explicit inf_rational(int n): m_first(rational(n)), m_second(rational()) @@ -470,5 +465,3 @@ inline inf_rational abs(const inf_rational & r) { } return result; } - -#endif /* INF_RATIONAL_H_ */ diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index dd136d1b9..b99167b32 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef INF_S_INTEGER_H_ -#define INF_S_INTEGER_H_ +#pragma once #include "util/s_integer.h" #include "util/rational.h" @@ -47,8 +46,6 @@ class inf_s_integer { inf_s_integer():m_first(0), m_second(0) {} - inf_s_integer(const inf_s_integer & r):m_first(r.m_first), m_second(r.m_second) {} - 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); } explicit inf_s_integer(s_integer const& r, bool pos_inf):m_first(r.get_int()), m_second(pos_inf ? 1 : -1) {} @@ -345,7 +342,3 @@ inline inf_s_integer abs(const inf_s_integer & r) { } return result; } - - -#endif /* INF_S_INTEGER_H_ */ - diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index e3b0d0710..6b00f894f 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef OBJ_REF_H_ -#define OBJ_REF_H_ +#pragma once /** Smart pointer for T objects. @@ -53,7 +52,7 @@ public: inc_ref(); } - obj_ref(obj_ref && other) : m_obj(nullptr), m_manager(other.m_manager) { + obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) { std::swap(m_obj, other.m_obj); } @@ -146,5 +145,3 @@ inline void dec_range_ref(IT const & begin, IT const & end, TManager & m) { } } } - -#endif /* OBJ_REF_H_ */ diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index ce8060cd3..40c01b012 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -191,6 +191,13 @@ public: push_back(data[i]); } + void operator=(ref_vector_core && other) { + if (this != &other) { + reset(); + m_nodes = std::move(other.m_nodes); + } + } + void swap(unsigned idx1, unsigned idx2) { std::swap(m_nodes[idx1], m_nodes[idx2]); } @@ -234,7 +241,7 @@ public: this->append(other); } - ref_vector(ref_vector && other) : super(std::move(other)) {} + ref_vector(ref_vector &&) = default; ref_vector(TManager & m, unsigned sz, T * const * data): super(ref_manager_wrapper(m)) { @@ -320,6 +327,11 @@ public: // prevent abuse: ref_vector & operator=(ref_vector const & other) = delete; + ref_vector & operator=(ref_vector && other) { + super::operator=(std::move(other)); + return *this; + } + bool operator==(ref_vector const& other) const { if (other.size() != this->size()) return false; for (unsigned i = this->size(); i-- > 0; ) { diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h index 2c80c4703..3b35a1bd8 100644 --- a/src/util/scoped_numeral.h +++ b/src/util/scoped_numeral.h @@ -17,8 +17,7 @@ Author: Revision History: --*/ -#ifndef SCOPED_NUMERAL_H_ -#define SCOPED_NUMERAL_H_ +#pragma once template class _scoped_numeral { @@ -30,6 +29,7 @@ private: public: _scoped_numeral(Manager & m):m_manager(m) {} _scoped_numeral(_scoped_numeral const & n):m_manager(n.m_manager) { m().set(m_num, n.m_num); } + _scoped_numeral(_scoped_numeral &&) = default; ~_scoped_numeral() { m_manager.del(m_num); } Manager & m() const { return m_manager; } @@ -189,5 +189,3 @@ public: } }; - -#endif diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index cb9a6b4fd..f53d93470 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -16,17 +16,24 @@ Author: Revision History: --*/ -#ifndef SCOPED_NUMERAL_VECTOR_H_ -#define SCOPED_NUMERAL_VECTOR_H_ +#pragma once #include "util/vector.h" template class _scoped_numeral_vector : public svector { Manager & m_manager; - _scoped_numeral_vector(_scoped_numeral_vector const & v); public: _scoped_numeral_vector(Manager & m):m_manager(m) {} + + _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) { + for (unsigned i = 0, e = other.size(); i != e; ++i) { + push_back((*this)[i]); + } + } + + _scoped_numeral_vector(_scoped_numeral_vector&&) = default; + ~_scoped_numeral_vector() { reset(); } @@ -66,5 +73,3 @@ public: svector::resize(sz, 0); } }; - -#endif diff --git a/src/util/uint_set.h b/src/util/uint_set.h index ebef623aa..46a606e8f 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef UINT_SET_H_ -#define UINT_SET_H_ +#pragma once #include "util/util.h" #include "util/vector.h" @@ -29,16 +28,6 @@ public: typedef unsigned data; - uint_set() {} - - uint_set(const uint_set & source) { - for (unsigned i = 0; i < source.size(); ++i) { - push_back(source[i]); - } - } - - ~uint_set() {} - void swap(uint_set & other) { unsigned_vector::swap(other); } @@ -384,6 +373,3 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) { for (unsigned i : s) out << i << " "; return out; } - -#endif /* UINT_SET_H_ */ -