From a1bcf136a6c3a5cec5522cebd34b99ebbec90a8c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Aug 2024 17:34:54 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 1 - src/util/vector.h | 576 +++++++++++++++++++++++++++++++++++----- 2 files changed, 506 insertions(+), 71 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 84cdc6e6924..c11084e5669 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -99,7 +99,6 @@ namespace smt { m_model_generator->set_context(this); } - :: /** \brief retrieve flag for when cancelation is possible. */ diff --git a/src/util/vector.h b/src/util/vector.h index d684f43ebe8..e8ccf5ae834 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -45,120 +45,556 @@ Revision History: template using std_vector = std::vector>; -#if 0 - -// portability guide to std::vector. -// memory allocator should be based on memory_allocator -// -// template -// struct memory_allocator { -// typedef T value_type; -// etc (interface seems to change between C++17, 20 versions) -// }; -// - -// Note: -// polynomial.h contains declaration -// typedef svector numeral_vector; -// it is crucial that it uses svector and not vector. The destructors on elements of the numeral vector are handled outside. -// Numeral gets instantiated by mpz and mpz does not support copy constructors. -// porting svector to vector is therefore blocked on the semantics of svector being -// copy-constructor free. -// +#if 1 -#include +template +class vector { + SZ m_capacity = 0; + SZ m_size = 0; + T* m_data = nullptr; + + void destroy_elements() { + std::destroy_n(m_data, size()); + } + + void free_memory() { + memory::deallocate(m_data); + m_data = nullptr; + } + + void expand_vector() { + // ensure that the data is sufficiently aligned + // better fail to compile than produce code that may crash + + if (m_data == nullptr) { + m_capacity = 2; + m_size = 0; + m_data = reinterpret_cast(memory::allocate(sizeof(T) * m_capacity)); + } + else { + static_assert(std::is_nothrow_move_constructible::value); + SASSERT(capacity() > 0); + SZ old_capacity = m_capacity; + SZ new_capacity = (3 * old_capacity + 1) >> 1; + if (new_capacity <= old_capacity) { + throw default_exception("Overflow encountered when expanding vector"); + } + if (std::is_trivially_copyable::value) { + m_data = (T*)memory::reallocate(m_data, new_capacity); + } + else { + T* new_data = (T*)memory::allocate(new_capacity); + auto old_size = size(); + std::uninitialized_move_n(m_data, old_size, new_data); + destroy(); + m_data = new_data; + } + m_capacity = new_capacity; + } + } + + void copy_core(vector const& source) { + SASSERT(!m_data); + SZ size = source.size(); + SZ capacity = source.capacity(); + m_data = reinterpret_cast(memory::allocate(sizeof(T) * capacity)); + m_capacity = capacity; + m_size = size; + std::uninitialized_copy(source.begin(), source.end(), begin()); + } + + void destroy() { + if (m_data) { + if (CallDestructors) + destroy_elements(); + free_memory(); + } + } -template -class vector : public std::vector { public: typedef T data_t; - typedef typename std::vector::iterator iterator; + typedef T* iterator; + typedef const T* const_iterator; + + vector() = default; - vector() {} vector(SZ s) { - // TODO resize(s, T()); + init(s); + } + + void init(SZ s) { + SASSERT(m_data == nullptr); + if (s == 0) { + return; + } + m_data = reinterpret_cast(memory::allocate(sizeof(T) * s)); + m_capacity = s; + m_size = s; + // initialize elements + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + new (it) T(); + } } - vector(SZ s, T const& e) { - // TODO resize(s, e); + + vector(SZ s, T const& elem) { + resize(s, elem); } - vector(SZ s, T const* e) { - // TODO + vector(vector const& source) { + if (source.m_data) { + copy_core(source); + } + SASSERT(size() == source.size()); } - void reset() { clear(); } - void finalize() { clear(); } - void reserve(SZ s, T const & d) { - if (s > size()) - resize(s, d); + vector(vector&& other) noexcept { + std::swap(m_data, other.m_data); } - void reserve(SZ s) { - + + vector(SZ s, T const* data) { + for (SZ i = 0; i < s; i++) { + push_back(data[i]); + } } - void setx(SZ idx, T const & elem, T const & d) { - if (idx >= size()) - resize(idx+1, d); - (*this)[idx] = elem; + + ~vector() { + destroy(); } - T const & get(SZ idx, T const & d) const { - if (idx >= size()) { - return d; + void finalize() { + destroy(); + m_data = nullptr; + } + + bool operator==(vector const& other) const { + if (this == &other) { + return true; + } + if (size() != other.size()) + return false; + for (unsigned i = 0; i < size(); i++) { + if ((*this)[i] != other[i]) + return false; } - return (*this)[idx]; + return true; } - void insert(T const & elem) { + bool operator!=(vector const& other) const { + return !(*this == other); + } + + vector& operator=(vector const& source) { + if (this == &source) { + return *this; + } + destroy(); + if (source.m_data) + copy_core(source); + return *this; + } + + vector& operator=(vector&& source) noexcept { + if (this == &source) { + return *this; + } + destroy(); + std::swap(m_data, source.m_data); + return *this; + } + + bool containsp(std::function& predicate) const { + for (auto const& t : *this) + if (predicate(t)) + return true; + return false; + } + + /** + * retain elements that satisfy predicate. aka 'where'. + */ + vector filter_pure(std::function& predicate) const { + vector result; + for (auto& t : *this) + if (predicate(t)) + result.push_back(t); + return result; + } + + vector& filter_update(std::function& predicate) { + unsigned j = 0; + for (auto& t : *this) + if (predicate(t)) + set(j++, t); + shrink(j); + return *this; + } + + /** + * update elements using f, aka 'select' + */ + template + vector map_pure(std::function& f) const { + vector result; + for (auto& t : *this) + result.push_back(f(t)); + return result; + } + + vector& map_update(std::function& f) { + unsigned j = 0; + for (auto& t : *this) + set(j++, f(t)); + return *this; + } + + void reset() { + if (m_data) { + if (CallDestructors) { + destroy_elements(); + } + m_size = 0; + } + } + + void clear() { reset(); } + + bool empty() const { + return m_data == nullptr || m_size == 0; + } + + SZ size() const { + if (m_data == nullptr) { + return 0; + } + return m_size; + } + + SZ capacity() const { + if (m_data == nullptr) { + return 0; + } + return m_capacity; + } + + iterator begin() { + return m_data; + } + + iterator end() { + return m_data + size(); + } + + const_iterator begin() const { + return m_data; + } + + const_iterator end() const { + return m_data + size(); + } + + class reverse_iterator { + T* v; + public: + reverse_iterator(T* v) :v(v) {} + + T operator*() { return *v; } + reverse_iterator operator++(int) { + reverse_iterator tmp = *this; + --v; + return tmp; + } + reverse_iterator& operator++() { + --v; + return *this; + } + + bool operator==(reverse_iterator const& other) const { + return other.v == v; + } + bool operator!=(reverse_iterator const& other) const { + return other.v != v; + } + }; + + reverse_iterator rbegin() { return reverse_iterator(end() - 1); } + reverse_iterator rend() { return reverse_iterator(begin() - 1); } + + void set_end(iterator it) { + if (m_data) { + SZ new_sz = static_cast(it - m_data); + if (CallDestructors) { + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + m_size = new_sz; + } + else { + SASSERT(it == 0); + } + } + + T& operator[](SZ idx) { + SASSERT(idx < size()); + return m_data[idx]; + } + + T const& operator[](SZ idx) const { + SASSERT(idx < size()); + return m_data[idx]; + } + + T& get(SZ idx) { + SASSERT(idx < size()); + return m_data[idx]; + } + + T const& get(SZ idx) const { + SASSERT(idx < size()); + return m_data[idx]; + } + + void set(SZ idx, T const& val) { + SASSERT(idx < size()); + m_data[idx] = val; + } + + void set(SZ idx, T&& val) { + SASSERT(idx < size()); + m_data[idx] = std::move(val); + } + + T& back() { + SASSERT(!empty()); + return operator[](size() - 1); + } + + T const& back() const { + SASSERT(!empty()); + return operator[](size() - 1); + } + + void pop_back() { + SASSERT(!empty()); + if (CallDestructors) { + back().~T(); + } + m_size--; + } + + vector& push_back(T const& elem) { + if (m_data == nullptr || m_size == m_capacity) { + expand_vector(); + } + new (m_data + m_size) T(elem); + m_size++; + return *this; + } + + template + vector& push_back(T const& elem, T elem2, Args ... elems) { push_back(elem); + push_back(elem2, elems ...); + return *this; } - - void erase(iterator pos) { - // TODO + + vector& push_back(T&& elem) { + if (m_data == nullptr || m_size == m_capacity) { + expand_vector(); + } + new (m_data + m_size) T(std::move(elem)); + ++m_size; + return *this; } - void erase(T const& e) { - // TODO + void insert(T const& elem) { + push_back(elem); } - void fill(T const & elem) { - for (auto& e : *this) - e = elem; + + void erase(iterator pos) { + SASSERT(pos >= begin() && pos < end()); + iterator prev = pos; + ++pos; + iterator e = end(); + for (; pos != e; ++pos, ++prev) { + *prev = std::move(*pos); + } + pop_back(); } - void fill(unsigned sz, T const & elem) { - resize(sz); - fill(elem); + void erase(T const& elem) { + iterator it = std::find(begin(), end(), elem); + if (it != end()) { + erase(it); + } + } + + /** Erase all elements that satisfy the given predicate. Returns the number of erased elements. */ + template + SZ erase_if(UnaryPredicate should_erase) { + iterator i = begin(); + iterator const e = end(); + for (iterator j = begin(); j != e; ++j) + if (!should_erase(std::as_const(*j))) + *(i++) = std::move(*j); + SZ const count = e - i; + SASSERT_EQ(i - begin(), size() - count); + shrink(size() - count); + return count; } void shrink(SZ s) { - resize(s); + if (m_data) { + SASSERT(s <= m_size); + if (CallDestructors) { + iterator it = m_data + s; + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + m_size = s; + } + else { + SASSERT(s == 0); + } } - void reverse() { + + template + void resize(SZ s, Args args...) { SZ sz = size(); - for (SZ i = 0; i < sz/2; ++i) { - std::swap((*this)[i], (*this)[sz-i-1]); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + m_size = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(std::forward(args)); } } - void append(vector const & other) { - for(SZ i = 0; i < other.size(); ++i) { + void resize(SZ s) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + m_size = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(); + } + } + + void append(vector const& other) { + for (SZ i = 0; i < other.size(); ++i) { push_back(other[i]); } } - void append(unsigned n, T const* elems) { - // TODO + void append(SZ sz, T const* data) { + for (SZ i = 0; i < sz; ++i) { + push_back(data[i]); + } } - bool contains(T const & elem) const { - for (auto const& e : *this) - if (e == elem) + void init(vector const& other) { + if (this == &other) + return; + reset(); + append(other); + } + + void init(SZ sz, T const* data) { + reset(); + append(sz, data); + } + + T* data() const { + return m_data; + } + + void swap(vector& other) noexcept { + std::swap(m_data, other.m_data); + } + + void reverse() { + SZ sz = size(); + for (SZ i = 0; i < sz / 2; ++i) { + std::swap(m_data[i], m_data[sz - i - 1]); + } + } + + void fill(T const& elem) { + iterator i = begin(); + iterator e = end(); + for (; i != e; ++i) { + *i = elem; + } + } + + void fill(unsigned sz, T const& elem) { + resize(sz); + fill(elem); + } + + bool contains(T const& elem) const { + const_iterator it = begin(); + const_iterator e = end(); + for (; it != e; ++it) { + if (*it == elem) { return true; + } + } return false; } - -}; + // set pos idx with elem. If idx >= size, then expand using default. + void setx(SZ idx, T const& elem, T const& d) { + if (idx >= size()) { + resize(idx + 1, d); + } + m_data[idx] = elem; + } + + // return element at position idx, if idx >= size, then return default + T const& get(SZ idx, T const& d) const { + if (idx >= size()) { + return d; + } + return m_data[idx]; + } + + void reserve(SZ s, T const& d) { + if (s > size()) + resize(s, d); + } + + void reserve(SZ s) { + if (s > size()) + resize(s); + } + + struct scoped_stack { + vector& s; + unsigned sz; + scoped_stack(vector& s) :s(s), sz(s.size()) {} + ~scoped_stack() { s.shrink(sz); } + }; + +}; + + + #else