From 82d853e5f8c15ec54849cdfe9eac7f3037425c9e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 1 Aug 2022 22:45:50 +0700 Subject: [PATCH] Use `= delete` to delete special methods. This provides a better experience than just marking them as private and leaving them as undefined symbols. --- src/ast/pattern/pattern_inference.h | 4 ++-- src/muz/base/dl_costs.h | 6 ++---- src/muz/base/dl_rule_subsumption_index.h | 6 ++---- src/muz/rel/dl_base.h | 21 +++++++++------------ src/muz/rel/dl_mk_simple_joins.cpp | 3 +-- src/muz/transforms/dl_mk_slice.cpp | 4 ++-- src/util/array.h | 4 ++-- src/util/params.h | 3 ++- src/util/scoped_numeral_buffer.h | 3 ++- 9 files changed, 24 insertions(+), 30 deletions(-) diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index d036ad789..28218ee17 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -48,14 +48,14 @@ class smaller_pattern { void save(expr * p1, expr * p2); bool process(expr * p1, expr * p2); - smaller_pattern & operator=(smaller_pattern const &); - public: smaller_pattern(ast_manager & m): m(m) { } + smaller_pattern & operator=(smaller_pattern const &) = delete; + bool operator()(unsigned num_bindings, expr * p1, expr * p2); }; diff --git a/src/muz/base/dl_costs.h b/src/muz/base/dl_costs.h index 333dac996..ea3efcda9 100644 --- a/src/muz/base/dl_costs.h +++ b/src/muz/base/dl_costs.h @@ -80,10 +80,8 @@ namespace datalog { bool passes_output_thresholds(context & ctx) const; void output_profile(std::ostream & out) const; - private: - //private and undefined copy constructor and operator= to avoid the default ones - accounted_object(const accounted_object &); - accounted_object& operator=(const accounted_object &); + accounted_object(const accounted_object &) = delete; + accounted_object& operator=(const accounted_object &) = delete; }; diff --git a/src/muz/base/dl_rule_subsumption_index.h b/src/muz/base/dl_rule_subsumption_index.h index 02f373377..9c29683b3 100644 --- a/src/muz/base/dl_rule_subsumption_index.h +++ b/src/muz/base/dl_rule_subsumption_index.h @@ -25,10 +25,6 @@ Revision History: namespace datalog { class rule_subsumption_index { - //private and undefined copy constroctor - rule_subsumption_index(rule_subsumption_index const&); - //private and undefined operator= - rule_subsumption_index& operator=(rule_subsumption_index const&); typedef obj_hashtable app_set; @@ -53,6 +49,8 @@ namespace datalog { reset_dealloc_values(m_unconditioned_heads); } + rule_subsumption_index(rule_subsumption_index const&) = delete; + rule_subsumption_index& operator=(rule_subsumption_index const&) = delete; void add(rule * r); bool is_subsumed(rule * r); bool is_subsumed(app * query); diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index f0634f0d5..1a4125ed4 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -180,10 +180,9 @@ namespace datalog { public: base_fn() = default; virtual ~base_fn() {} - private: - //private and undefined copy constructor and operator= to avoid copying - base_fn(const base_fn &); - base_fn& operator=(const base_fn &); + + base_fn(const base_fn &) = delete; + base_fn& operator=(const base_fn &) = delete; }; class join_fn : public base_fn { @@ -1098,6 +1097,9 @@ namespace datalog { iterator_core() : m_ref_cnt(0) {} virtual ~iterator_core() {} + iterator_core(const iterator_core &) = delete; + iterator_core & operator=(const iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1116,10 +1118,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - iterator_core(const iterator_core &); - iterator_core & operator=(const iterator_core &); }; struct row_iterator_core { @@ -1128,6 +1126,9 @@ namespace datalog { row_iterator_core() : m_ref_cnt(0) {} virtual ~row_iterator_core() {} + row_iterator_core(const row_iterator_core &) = delete; + row_iterator_core & operator=(const row_iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1146,10 +1147,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - row_iterator_core(const row_iterator_core &); - row_iterator_core & operator=(const row_iterator_core &); }; public: diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index 3fa52ae2f..37fd3ef36 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -56,6 +56,7 @@ namespace datalog { pair_info() {} + pair_info & operator=(const pair_info &) = delete; bool can_be_joined() const { return m_consumers > 0; } @@ -110,8 +111,6 @@ namespace datalog { SASSERT(!m_rules.empty() || m_consumers == 0); return m_rules.empty(); } - private: - pair_info & operator=(const pair_info &); //to avoid the implicit one }; typedef std::pair app_pair; typedef pair_hash, obj_ptr_hash > app_pair_hash; diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 28cbf638e..eda00b64d 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -111,8 +111,6 @@ namespace datalog { rule_unifier m_unifier; - slice_proof_converter(slice_proof_converter const& other); - void init_form2rule() { if (!m_sliceform2rule.empty()) { return; @@ -271,6 +269,8 @@ namespace datalog { m_renaming.insert(orig_rule, unsigned_vector(sz, renaming)); } + slice_proof_converter(slice_proof_converter const& other) = delete; + proof_ref operator()(ast_manager& m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 1); proof_ref result(source[0], m); diff --git a/src/util/array.h b/src/util/array.h index 6c04c10d2..a4c2aa2c7 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -37,8 +37,6 @@ private: char * raw_ptr() const { return reinterpret_cast(reinterpret_cast(m_data) - 1); } - array & operator=(array const & source); - void set_data(void * mem, unsigned sz) { size_t * _mem = static_cast(mem); *_mem = sz; @@ -115,6 +113,8 @@ public: destroy_elements(); } + array & operator=(array const & source) = delete; + // Free the memory used to store the array. template void finalize(Allocator & a) { diff --git a/src/util/params.h b/src/util/params.h index da05dff90..7ad152a59 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -35,13 +35,14 @@ class params_ref { params * m_params; void init(); void copy_core(params const * p); - params_ref& operator=(params_ref const& p) = delete; void set(params_ref const& p); public: params_ref():m_params(nullptr) {} params_ref(params_ref const & p); ~params_ref(); + params_ref& operator=(params_ref const& p) = delete; + static params_ref const & get_empty() { return g_empty_params_ref; } diff --git a/src/util/scoped_numeral_buffer.h b/src/util/scoped_numeral_buffer.h index 86181f761..81d10ba40 100644 --- a/src/util/scoped_numeral_buffer.h +++ b/src/util/scoped_numeral_buffer.h @@ -24,13 +24,14 @@ template class _scoped_numeral_buffer : public sbuffer { typedef sbuffer super; Manager & m_manager; - _scoped_numeral_buffer(_scoped_numeral_buffer const & v); public: _scoped_numeral_buffer(Manager & m):m_manager(m) {} ~_scoped_numeral_buffer() { reset(); } + _scoped_numeral_buffer(_scoped_numeral_buffer const & v) = delete; + void reset() { unsigned sz = this->size(); for (unsigned i = 0; i < sz; i++) {