mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

Use = delete to delete special methods.

Browse source 
This provides a better experience than just marking them as
private and leaving them as undefined symbols.
This commit is contained in:
Bruce Mitchener 2022-08-01 22:45:50 +07:00 committed by Nikolaj Bjorner
parent 059b795faa
commit 82d853e5f8
9 changed files with 24 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/pattern/pattern_inference.h
View file

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

6
src/muz/base/dl_costs.h
View file

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

6
src/muz/base/dl_rule_subsumption_index.h
View file

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

21
src/muz/rel/dl_base.h
View file

@ -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:

3
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -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*, app*> app_pair;
typedef pair_hash<obj_ptr_hash<app>, obj_ptr_hash<app> > app_pair_hash;

4
src/muz/transforms/dl_mk_slice.cpp
View file

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

4
src/util/array.h
View file

@ -37,8 +37,6 @@ private:
char * raw_ptr() const { return reinterpret_cast<char*>(reinterpret_cast<size_t*>(m_data) - 1); }
array & operator=(array const & source);
void set_data(void * mem, unsigned sz) {
size_t * _mem = static_cast<size_t*>(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<typename Allocator>
void finalize(Allocator & a) {

3
src/util/params.h
View file

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

3
src/util/scoped_numeral_buffer.h
View file

@ -24,13 +24,14 @@ template<typename Manager, unsigned INITIAL_SIZE = 16>
class _scoped_numeral_buffer : public sbuffer<typename Manager::numeral, INITIAL_SIZE> {
typedef sbuffer<typename Manager::numeral, INITIAL_SIZE> 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++) {