mirror of
https://github.com/Z3Prover/z3
synced 2025-08-26 04:56:03 +00:00
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..
This commit is contained in:
parent
e2b2b7f82e
commit
e844aef896
17 changed files with 44 additions and 95 deletions
|
@ -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<optional<entry>, 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_ */
|
||||
|
|
|
@ -17,8 +17,8 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef INF_RATIONAL_H_
|
||||
#define INF_RATIONAL_H_
|
||||
#pragma once
|
||||
|
||||
#include<stdlib.h>
|
||||
#include<string>
|
||||
#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_ */
|
||||
|
|
|
@ -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_ */
|
||||
|
||||
|
|
|
@ -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_ */
|
||||
|
|
|
@ -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<T, TManager>(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; ) {
|
||||
|
|
|
@ -17,8 +17,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef SCOPED_NUMERAL_H_
|
||||
#define SCOPED_NUMERAL_H_
|
||||
#pragma once
|
||||
|
||||
template<typename Manager>
|
||||
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
|
||||
|
|
|
@ -16,17 +16,24 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef SCOPED_NUMERAL_VECTOR_H_
|
||||
#define SCOPED_NUMERAL_VECTOR_H_
|
||||
#pragma once
|
||||
|
||||
#include "util/vector.h"
|
||||
|
||||
template<typename Manager>
|
||||
class _scoped_numeral_vector : public svector<typename Manager::numeral> {
|
||||
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<typename Manager::numeral>::resize(sz, 0);
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -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_ */
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue