mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

add rval methods to scoped_vector

Browse source
This commit is contained in:
Nuno Lopes 2020-07-12 22:16:24 +01:00
parent f30e8ccec3
commit 90fc8d854f
2 changed files with 22 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/ref_vector.h
View file

@ -324,11 +324,6 @@ public:
return *this; return *this;
} }
ref_vector & operator=(ref_vector const & other) {
set(other);
return *this;
}
ref_vector & operator=(ref_vector && other) = default; ref_vector & operator=(ref_vector && other) = default;
bool operator==(ref_vector const& other) const { bool operator==(ref_vector const& other) const {

22
src/util/scoped_vector.h
View file

@ -90,6 +90,19 @@ public:
SASSERT(invariant()); SASSERT(invariant());
} }
void set(unsigned idx, T && t) {
SASSERT(idx < m_size);
unsigned n = m_index[idx];
if (n >= m_elems_start) {
m_elems[n] = std::move(t);
}
else {
set_index(idx, m_elems.size());
m_elems.push_back(std::move(t));
}
SASSERT(invariant());
}
class iterator { class iterator {
scoped_vector const& m_vec; scoped_vector const& m_vec;
unsigned m_index; unsigned m_index;
@ -122,6 +135,13 @@ public:
SASSERT(invariant()); SASSERT(invariant());
} }
void push_back(T && t) {
set_index(m_size, m_elems.size());
m_elems.push_back(std::move(t));
++m_size;
SASSERT(invariant());
}
void pop_back() { void pop_back() {
SASSERT(m_size > 0); SASSERT(m_size > 0);
if (m_index[m_size-1] == m_elems.size()-1 && if (m_index[m_size-1] == m_elems.size()-1 &&
@ -135,7 +155,7 @@ public:
void erase_and_swap(unsigned i) { void erase_and_swap(unsigned i) {
if (i + 1 < size()) { if (i + 1 < size()) {
auto n = m_elems[m_index[size() - 1]]; auto n = m_elems[m_index[size() - 1]];
set(i, n); set(i, std::move(n));
} }
pop_back(); pop_back();
} }