3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00

import goodies from ps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-21 11:13:03 -07:00
parent 708602dfbb
commit de20bffafe
2 changed files with 22 additions and 1 deletions

View file

@ -269,6 +269,11 @@ public:
return *this; return *this;
} }
scoped_ptr& operator=(scoped_ptr&& other) {
*this = other.detach();
return *this;
};
T * detach() { T * detach() {
T* tmp = m_ptr; T* tmp = m_ptr;
m_ptr = nullptr; m_ptr = nullptr;

View file

@ -641,7 +641,7 @@ public:
return m_data; return m_data;
} }
void swap(vector & other) { void swap(vector & other) noexcept {
std::swap(m_data, other.m_data); std::swap(m_data, other.m_data);
} }
@ -720,6 +720,17 @@ public:
ptr_vector(unsigned s):vector<T *, false>(s) {} ptr_vector(unsigned s):vector<T *, false>(s) {}
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {} ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {} ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
std::ostream& display(std::ostream& out, char const* delim = " ") const {
char const* d = "";
for (auto const* u : *this) {
if (u)
out << d << *u;
else
out << d << "<NULL>";
d = delim;
}
return out;
}
}; };
template<typename T, typename SZ = unsigned> template<typename T, typename SZ = unsigned>
@ -746,6 +757,11 @@ inline std::ostream& operator<<(std::ostream& out, svector<T> const& v) {
return out; return out;
} }
template<typename T>
inline std::ostream& operator<<(std::ostream& out, ptr_vector<T> const& v) {
return v.display(out);
}
template<typename Hash, typename Vec> template<typename Hash, typename Vec>
struct vector_hash_tpl { struct vector_hash_tpl {