mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

buffer.h c++17 improvements

Browse source 
1) ensure data is properly aligned
2) add move constructor (useful for zstrings)
This commit is contained in:
Nuno Lopes 2021-05-23 12:11:12 +01:00
parent 34e8a2f0f6
commit 79201e5ce6
1 changed files with 25 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/util/buffer.h
View file

@ -27,11 +27,11 @@ Revision History:
template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
class buffer {
protected:
T * m_buffer;
unsigned m_pos;
unsigned m_capacity;
char m_initial_buffer[INITIAL_SIZE * sizeof(T)];
T * m_buffer = reinterpret_cast<T*>(m_initial_buffer);
unsigned m_pos = 0;
unsigned m_capacity = INITIAL_SIZE;
typename std::aligned_storage<sizeof(T), alignof(T)>::type m_initial_buffer[INITIAL_SIZE];
void free_memory() {
if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
dealloc_svect(m_buffer);
@ -39,7 +39,7 @@ protected:
}
void expand() {
static_assert(std::is_nothrow_move_constructible<T>::value, "");
static_assert(std::is_nothrow_move_constructible<T>::value);
unsigned new_capacity = m_capacity << 1;
T * new_buffer = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
for (unsigned i = 0; i < m_pos; ++i) {
@ -73,26 +73,29 @@ public:
typedef T * iterator;
typedef const T * const_iterator;
buffer():
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
}
buffer() = default;
buffer(const buffer & source):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
unsigned sz = source.size();
for(unsigned i = 0; i < sz; i++) {
buffer(const buffer & source) {
for (unsigned i = 0, sz = source.size(); i < sz; ++i) {
push_back(source.m_buffer[i]);
}
}
buffer(unsigned sz, const T & elem):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
buffer(buffer && source) {
if (source.m_buffer == reinterpret_cast<T*>(source.m_initial_buffer)) {
for (unsigned i = 0, sz = source.size(); i < sz; ++i) {
push_back(std::move(source.m_buffer[i]));
}
} else {
m_pos = source.m_pos;
m_capacity = source.m_capacity;
m_buffer = source.m_buffer;
source.m_buffer = reinterpret_cast<T*>(source.m_initial_buffer);
source.m_pos = 0;
}
}
buffer(unsigned sz, const T & elem) {
for (unsigned i = 0; i < sz; i++) {
push_back(elem);
}