From 3845e0859c90f91bb886ed9c52aa93f5c429a3b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Apr 2020 12:23:18 -0700 Subject: [PATCH] fix #3878 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_common.cpp | 2 +- src/smt/theory_seq.cpp | 7 +- src/util/buffer.h | 262 ++++++++++++++- src/util/old_buffer.h | 270 ---------------- src/util/old_vector.h | 620 ------------------------------------ src/util/vector.h | 629 +++++++++++++++++++++++++++++++++++-- 6 files changed, 870 insertions(+), 920 deletions(-) delete mode 100644 src/util/old_buffer.h delete mode 100644 src/util/old_vector.h diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 4b51c577e..770e782c2 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -194,4 +194,4 @@ template void common::create_sum_from_row(const T& row, } -template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&); +template void nla::common::create_sum_from_row, true, unsigned int> >(vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index dfa9353bd..4125e9cc1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1640,6 +1640,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector & le len.push_back(rational(s.length())); } else if (get_length(e, val)) { + SASSERT(!val.is_neg()); len.push_back(val); } else { @@ -3916,6 +3917,8 @@ void theory_seq::add_itos_axiom(expr* e) { // itos(n) = "" or n >= 0 add_axiom(~eq1, ~ge0); add_axiom(eq1, ge0); + + add_axiom(mk_literal(m_autil.mk_ge(mk_len(e), m_autil.mk_int(0)))); // n >= 0 => stoi(itos(n)) = n app_ref stoi(m_util.str.mk_stoi(e), m); @@ -5240,8 +5243,8 @@ void theory_seq::add_itos_length_axiom(expr* len) { num_char2 = len2.get_unsigned(); } unsigned num_char = std::max(num_char1, num_char2); - + add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0)))); literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char)))); literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char)))); literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0)))); @@ -5519,7 +5522,7 @@ bool theory_seq::get_length(expr* e, rational& val) { } else { len = mk_len(c); - if (m_arith_value.get_value(len, val1)) { + if (m_arith_value.get_value(len, val1) && !val1.is_neg()) { val += val1; } else { diff --git a/src/util/buffer.h b/src/util/buffer.h index 0d32245d3..13a5ca00b 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -1,30 +1,274 @@ + /*++ -Copyright (c) 2019 Microsoft Corporation +Copyright (c) 2006 Microsoft Corporation Module Name: buffer.h +Abstract: + + + Author: - Daniel Schemmel 2019-2-23 + Leonardo de Moura (leonardo) 2006-10-16. + +Revision History: + --*/ - #ifndef BUFFER_H_ #define BUFFER_H_ -#include "old_buffer.h" +#include +#include "util/memory_manager.h" template -using buffer = old_buffer; +class buffer { +protected: + T * m_buffer; + unsigned m_pos; + unsigned m_capacity; + char m_initial_buffer[INITIAL_SIZE * sizeof(T)]; + + void free_memory() { + if (m_buffer != reinterpret_cast(m_initial_buffer)) { + dealloc_svect(m_buffer); + } + } -// note that the append added in the old_ptr_buffer is actually not an addition over its base class old_buffer, + void expand() { + unsigned new_capacity = m_capacity << 1; + T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); + memcpy(new_buffer, m_buffer, m_pos * sizeof(T)); + free_memory(); + m_buffer = new_buffer; + m_capacity = new_capacity; + } + + void destroy_elements() { + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + + void destroy() { + if (CallDestructors) { + destroy_elements(); + } + free_memory(); + } + +public: + typedef T data; + typedef T * iterator; + typedef const T * const_iterator; + + buffer(): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + } + + buffer(const buffer & source): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + unsigned sz = source.size(); + for(unsigned i = 0; i < sz; i++) { + push_back(source.m_buffer[i]); + } + } + + buffer(unsigned sz, const T & elem): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + for (unsigned i = 0; i < sz; i++) { + push_back(elem); + } + SASSERT(size() == sz); + } + + ~buffer() { + destroy(); + } + + void reset() { + if (CallDestructors) { + destroy_elements(); + } + m_pos = 0; + } + + void finalize() { + destroy(); + m_buffer = reinterpret_cast(m_initial_buffer); + m_pos = 0; + m_capacity = INITIAL_SIZE; + } + + unsigned size() const { + return m_pos; + } + + bool empty() const { + return m_pos == 0; + } + + iterator begin() { + return m_buffer; + } + + iterator end() { + return m_buffer + size(); + } + + void set_end(iterator it) { + m_pos = static_cast(it - m_buffer); + if (CallDestructors) { + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + } + + const_iterator begin() const { + return m_buffer; + } + + const_iterator end() const { + return m_buffer + size(); + } + + void push_back(const T & elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(elem); + m_pos++; + } + + void push_back(T && elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(std::move(elem)); + m_pos++; + } + + void pop_back() { + if (CallDestructors) { + back().~T(); + } + m_pos--; + } + + const T & back() const { + SASSERT(!empty()); + SASSERT(m_pos > 0); + return m_buffer[m_pos - 1]; + } + + T & back() { + SASSERT(!empty()); + SASSERT(m_pos > 0); + return m_buffer[m_pos - 1]; + } + + T * c_ptr() const { + return m_buffer; + } + + void append(unsigned n, T const * elems) { + for (unsigned i = 0; i < n; i++) { + push_back(elems[i]); + } + } + + void append(const buffer& source) { + append(source.size(), source.c_ptr()); + } + + T & operator[](unsigned idx) { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + const T & operator[](unsigned idx) const { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + T & get(unsigned idx) { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + const T & get(unsigned idx) const { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + void set(unsigned idx, T const & val) { + SASSERT(idx < size()); + m_buffer[idx] = val; + } + + void resize(unsigned nsz, const T & elem=T()) { + unsigned sz = size(); + if (nsz > sz) { + for (unsigned i = sz; i < nsz; i++) { + push_back(elem); + } + } + else if (nsz < sz) { + for (unsigned i = nsz; i < sz; i++) { + pop_back(); + } + } + SASSERT(size() == nsz); + } + + void shrink(unsigned nsz) { + unsigned sz = size(); + SASSERT(nsz <= sz); + for (unsigned i = nsz; i < sz; i++) + pop_back(); + SASSERT(size() == nsz); + } + + buffer & operator=(buffer const & other) { + if (this == &other) + return *this; + reset(); + append(other); + return *this; + } +}; + +// note that the append added is actually not an addition over its base class buffer, // which already has an append function with the same signature and implementation -template -using ptr_buffer = old_ptr_buffer; template -using sbuffer = old_sbuffer; +class ptr_buffer : public buffer { +public: + void append(unsigned n, T * const * elems) { + for (unsigned i = 0; i < n; i++) { + this->push_back(elems[i]); + } + } +}; + +template +class sbuffer : public buffer { +public: + sbuffer(): buffer() {} + sbuffer(unsigned sz, const T& elem) : buffer(sz,elem) {} +}; + + #endif /* BUFFER_H_ */ diff --git a/src/util/old_buffer.h b/src/util/old_buffer.h deleted file mode 100644 index 88800b05a..000000000 --- a/src/util/old_buffer.h +++ /dev/null @@ -1,270 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - old_buffer.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2006-10-16. - -Revision History: - - 2019-2-23 Renamed to old_buffer from buffer to provide new implementation - ---*/ -#ifndef OLD_BUFFER_H_ -#define OLD_BUFFER_H_ - -#include -#include "util/memory_manager.h" - -template -class old_buffer { -protected: - T * m_buffer; - unsigned m_pos; - unsigned m_capacity; - char m_initial_buffer[INITIAL_SIZE * sizeof(T)]; - - void free_memory() { - if (m_buffer != reinterpret_cast(m_initial_buffer)) { - dealloc_svect(m_buffer); - } - } - - void expand() { - unsigned new_capacity = m_capacity << 1; - T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); - memcpy(new_buffer, m_buffer, m_pos * sizeof(T)); - free_memory(); - m_buffer = new_buffer; - m_capacity = new_capacity; - } - - void destroy_elements() { - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - - void destroy() { - if (CallDestructors) { - destroy_elements(); - } - free_memory(); - } - -public: - typedef T data; - typedef T * iterator; - typedef const T * const_iterator; - - old_buffer(): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - } - - old_buffer(const old_buffer & source): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - unsigned sz = source.size(); - for(unsigned i = 0; i < sz; i++) { - push_back(source.m_buffer[i]); - } - } - - old_buffer(unsigned sz, const T & elem): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - for (unsigned i = 0; i < sz; i++) { - push_back(elem); - } - SASSERT(size() == sz); - } - - ~old_buffer() { - destroy(); - } - - void reset() { - if (CallDestructors) { - destroy_elements(); - } - m_pos = 0; - } - - void finalize() { - destroy(); - m_buffer = reinterpret_cast(m_initial_buffer); - m_pos = 0; - m_capacity = INITIAL_SIZE; - } - - unsigned size() const { - return m_pos; - } - - bool empty() const { - return m_pos == 0; - } - - iterator begin() { - return m_buffer; - } - - iterator end() { - return m_buffer + size(); - } - - void set_end(iterator it) { - m_pos = static_cast(it - m_buffer); - if (CallDestructors) { - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - } - - const_iterator begin() const { - return m_buffer; - } - - const_iterator end() const { - return m_buffer + size(); - } - - void push_back(const T & elem) { - if (m_pos >= m_capacity) - expand(); - new (m_buffer + m_pos) T(elem); - m_pos++; - } - - void push_back(T && elem) { - if (m_pos >= m_capacity) - expand(); - new (m_buffer + m_pos) T(std::move(elem)); - m_pos++; - } - - void pop_back() { - if (CallDestructors) { - back().~T(); - } - m_pos--; - } - - const T & back() const { - SASSERT(!empty()); - SASSERT(m_pos > 0); - return m_buffer[m_pos - 1]; - } - - T & back() { - SASSERT(!empty()); - SASSERT(m_pos > 0); - return m_buffer[m_pos - 1]; - } - - T * c_ptr() const { - return m_buffer; - } - - void append(unsigned n, T const * elems) { - for (unsigned i = 0; i < n; i++) { - push_back(elems[i]); - } - } - - void append(const old_buffer& source) { - append(source.size(), source.c_ptr()); - } - - T & operator[](unsigned idx) { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - const T & operator[](unsigned idx) const { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - T & get(unsigned idx) { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - const T & get(unsigned idx) const { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - void set(unsigned idx, T const & val) { - SASSERT(idx < size()); - m_buffer[idx] = val; - } - - void resize(unsigned nsz, const T & elem=T()) { - unsigned sz = size(); - if (nsz > sz) { - for (unsigned i = sz; i < nsz; i++) { - push_back(elem); - } - } - else if (nsz < sz) { - for (unsigned i = nsz; i < sz; i++) { - pop_back(); - } - } - SASSERT(size() == nsz); - } - - void shrink(unsigned nsz) { - unsigned sz = size(); - SASSERT(nsz <= sz); - for (unsigned i = nsz; i < sz; i++) - pop_back(); - SASSERT(size() == nsz); - } - - old_buffer & operator=(old_buffer const & other) { - if (this == &other) - return *this; - reset(); - append(other); - return *this; - } -}; - -template -class old_ptr_buffer : public old_buffer { -public: - void append(unsigned n, T * const * elems) { - for (unsigned i = 0; i < n; i++) { - this->push_back(elems[i]); - } - } -}; - -template -class old_sbuffer : public old_buffer { -public: - old_sbuffer(): old_buffer() {} - old_sbuffer(unsigned sz, const T& elem) : old_buffer(sz,elem) {} -}; - -#endif /* OLD_BUFFER_H_ */ - diff --git a/src/util/old_vector.h b/src/util/old_vector.h deleted file mode 100644 index 7f214803c..000000000 --- a/src/util/old_vector.h +++ /dev/null @@ -1,620 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - old_vector.h - -Abstract: - Dynamic array implementation. - Remarks: - - - Empty arrays consume only sizeof(T *) bytes. - - - There is the option of disabling the destructor invocation for elements stored in the vector. - This is useful for vectors of int. - -Author: - - Leonardo de Moura (leonardo) 2006-09-11. - -Revision History: - - 2019-2-23 Renamed from vector to old_vector to provide new implementation - ---*/ -#ifndef OLD_VECTOR_H_ -#define OLD_VECTOR_H_ - -#include "util/debug.h" -#include -#include -#include -#include -#include "util/memory_manager.h" -#include "util/hash.h" -#include "util/z3_exception.h" - -// disable warning for constant 'if' expressions. -// these are used heavily in templates. -#ifdef _MSC_VER -#pragma warning(disable:4127) -#endif - -template -class old_vector { -#define SIZE_IDX -1 -#define CAPACITY_IDX -2 - T * m_data; - - void destroy_elements() { - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - - void free_memory() { - memory::deallocate(reinterpret_cast(reinterpret_cast(m_data) - 2)); - } - - void expand_vector() { - if (m_data == nullptr) { - SZ capacity = 2; - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); - *mem = capacity; - mem++; - *mem = 0; - mem++; - m_data = reinterpret_cast(mem); - } - else { - SASSERT(capacity() > 0); - SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; - SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; - SZ new_capacity = (3 * old_capacity + 1) >> 1; - SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; - if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { - throw default_exception("Overflow encountered when expanding old_vector"); - } - SZ *mem, *old_mem = reinterpret_cast(m_data) - 2; -#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5 - if (__has_trivial_copy(T)) { -#else - if (std::is_trivially_copyable::value) { -#endif - mem = (SZ*)memory::reallocate(old_mem, new_capacity_T); - m_data = reinterpret_cast(mem + 2); - } else { - mem = (SZ*)memory::allocate(new_capacity_T); - auto old_data = m_data; - auto old_size = size(); - mem[1] = old_size; - m_data = reinterpret_cast(mem + 2); - for (unsigned i = 0; i < old_size; ++i) { - new (&m_data[i]) T(std::move(old_data[i])); - old_data[i].~T(); - } - memory::deallocate(old_mem); - } - *mem = new_capacity; - } - } - - void copy_core(old_vector const & source) { - SZ size = source.size(); - SZ capacity = source.capacity(); - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); - *mem = capacity; - mem++; - *mem = size; - mem++; - m_data = reinterpret_cast(mem); - const_iterator it = source.begin(); - iterator it2 = begin(); - SASSERT(it2 == m_data); - const_iterator e = source.end(); - for (; it != e; ++it, ++it2) { - new (it2) T(*it); - } - } - - void destroy() { - if (m_data) { - if (CallDestructors) { - destroy_elements(); - } - free_memory(); - } - } - -public: - typedef T data; - typedef T * iterator; - typedef const T * const_iterator; - - old_vector(): - m_data(nullptr) { - } - - old_vector(SZ s) { - if (s == 0) { - m_data = nullptr; - return; - } - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2)); - *mem = s; - mem++; - *mem = s; - mem++; - m_data = reinterpret_cast(mem); - // initialize elements - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - new (it) T(); - } - } - - old_vector(SZ s, T const & elem): - m_data(nullptr) { - resize(s, elem); - } - - old_vector(old_vector const & source): - m_data(nullptr) { - if (source.m_data) { - copy_core(source); - } - SASSERT(size() == source.size()); - } - - old_vector(old_vector&& other) : m_data(nullptr) { - std::swap(m_data, other.m_data); - } - - old_vector(SZ s, T const * data): - m_data(nullptr) { - for (SZ i = 0; i < s; i++) { - push_back(data[i]); - } - } - - - ~old_vector() { - destroy(); - } - - void finalize() { - destroy(); - m_data = nullptr; - } - - bool operator==(old_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 true; - } - - bool operator!=(old_vector const & other) const { - return !(*this == other); - } - - - old_vector & operator=(old_vector const & source) { - if (this == &source) { - return *this; - } - destroy(); - if (source.m_data) { - copy_core(source); - } - else { - m_data = nullptr; - } - return *this; - } - - old_vector & operator=(old_vector && source) { - if (this == &source) { - return *this; - } - destroy(); - m_data = nullptr; - 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'. - */ - old_vector filter_pure(std::function& predicate) const { - old_vector result; - for (auto& t : *this) - if (predicate(t)) - result.push_back(t); - return result; - } - - old_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 - old_vector map_pure(std::function& f) const { - old_vector result; - for (auto& t : *this) - result.push_back(f(t)); - return result; - } - - old_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(); - } - reinterpret_cast(m_data)[SIZE_IDX] = 0; - } - } - - void clear() { reset(); } - - bool empty() const { - return m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == 0; - } - - SZ size() const { - if (m_data == nullptr) { - return 0; - } - return reinterpret_cast(m_data)[SIZE_IDX]; - } - - SZ capacity() const { - if (m_data == nullptr) { - return 0; - } - return reinterpret_cast(m_data)[CAPACITY_IDX]; - } - - 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(); - } - } - reinterpret_cast(m_data)[SIZE_IDX] = 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(); - } - reinterpret_cast(m_data)[SIZE_IDX]--; - } - - old_vector& push_back(T const & elem) { - if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { - expand_vector(); - } - new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); - reinterpret_cast(m_data)[SIZE_IDX]++; - return *this; - } - - template - old_vector& push_back(T const& elem, T elem2, Args ... elems) { - push_back(elem); - push_back(elem2, elems ...); - return *this; - } - - old_vector& push_back(T && elem) { - if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { - expand_vector(); - } - new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); - reinterpret_cast(m_data)[SIZE_IDX]++; - return *this; - } - - void insert(T const & elem) { - push_back(elem); - } - - void erase(iterator pos) { - SASSERT(pos >= begin() && pos < end()); - iterator prev = pos; - ++pos; - iterator e = end(); - for(; pos != e; ++pos, ++prev) { - *prev = *pos; - } - reinterpret_cast(m_data)[SIZE_IDX]--; - } - - void erase(T const & elem) { - iterator it = std::find(begin(), end(), elem); - if (it != end()) { - erase(it); - } - } - - void shrink(SZ s) { - if (m_data) { - SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); - if (CallDestructors) { - iterator it = m_data + s; - iterator e = end(); - for(; it != e; ++it) { - it->~T(); - } - } - reinterpret_cast(m_data)[SIZE_IDX] = s; - } - else { - SASSERT(s == 0); - } - } - - template - void resize(SZ s, Args args...) { - SZ sz = size(); - if (s <= sz) { shrink(s); return; } - while (s > capacity()) { - expand_vector(); - } - SASSERT(m_data != 0); - reinterpret_cast(m_data)[SIZE_IDX] = s; - iterator it = m_data + sz; - iterator end = m_data + s; - for (; it != end; ++it) { - new (it) T(std::forward(args)); - } - } - - void resize(SZ s) { - SZ sz = size(); - if (s <= sz) { shrink(s); return; } - while (s > capacity()) { - expand_vector(); - } - SASSERT(m_data != 0); - reinterpret_cast(m_data)[SIZE_IDX] = s; - iterator it = m_data + sz; - iterator end = m_data + s; - for (; it != end; ++it) { - new (it) T(); - } - } - - void append(old_vector const & other) { - for(SZ i = 0; i < other.size(); ++i) { - push_back(other[i]); - } - } - - void append(SZ sz, T const * data) { - for(SZ i = 0; i < sz; ++i) { - push_back(data[i]); - } - } - - T * c_ptr() const { - return m_data; - } - - void swap(old_vector & other) { - 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); - } -}; - -template -class old_ptr_vector : public old_vector { -public: - old_ptr_vector():old_vector() {} - old_ptr_vector(unsigned s):old_vector(s) {} - old_ptr_vector(unsigned s, T * elem):old_vector(s, elem) {} - old_ptr_vector(old_ptr_vector const & source):old_vector(source) {} - old_ptr_vector(old_ptr_vector && other) : old_vector(std::move(other)) {} - old_ptr_vector(unsigned s, T * const * data):old_vector(s, const_cast(data)) {} - old_ptr_vector & operator=(old_ptr_vector const & source) { - old_vector::operator=(source); - return *this; - } -}; - -template -class old_svector : public old_vector { -public: - old_svector():old_vector() {} - old_svector(SZ s):old_vector(s) {} - old_svector(SZ s, T const & elem):old_vector(s, elem) {} - old_svector(old_svector const & source):old_vector(source) {} - old_svector(old_svector && other) : old_vector(std::move(other)) {} - old_svector(SZ s, T const * data):old_vector(s, data) {} - old_svector & operator=(old_svector const & source) { - old_vector::operator=(source); - return *this; - } -}; - -#endif /* OLD_VECTOR_H_ */ diff --git a/src/util/vector.h b/src/util/vector.h index 8a9e824b4..f94fda4f0 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -1,40 +1,633 @@ /*++ -Copyright (c) 2019 Microsoft Corporation +Copyright (c) 2006 Microsoft Corporation Module Name: vector.h +Abstract: + Dynamic array implementation. + Remarks: + + - Empty arrays consume only sizeof(T *) bytes. + + - There is the option of disabling the destructor invocation for elements stored in the vector. + This is useful for vectors of int. + Author: - Daniel Schemmel 2019-2-23 + Leonardo de Moura (leonardo) 2006-09-11. + +Revision History: + + 2019-2-23 Renamed from vector to vector to provide new implementation --*/ - #ifndef VECTOR_H_ #define VECTOR_H_ -#include "old_vector.h" -#include "hash.h" +#include "util/debug.h" +#include +#include +#include +#include +#include "util/memory_manager.h" +#include "util/hash.h" +#include "util/z3_exception.h" + +// disable warning for constant 'if' expressions. +// these are used heavily in templates. +#ifdef _MSC_VER +#pragma warning(disable:4127) +#endif template -using vector = old_vector; +class vector { +#define SIZE_IDX -1 +#define CAPACITY_IDX -2 + T * m_data; + + void destroy_elements() { + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + + void free_memory() { + memory::deallocate(reinterpret_cast(reinterpret_cast(m_data) - 2)); + } + + void expand_vector() { + if (m_data == nullptr) { + SZ capacity = 2; + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); + *mem = capacity; + mem++; + *mem = 0; + mem++; + m_data = reinterpret_cast(mem); + } + else { + SASSERT(capacity() > 0); + SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; + SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; + SZ new_capacity = (3 * old_capacity + 1) >> 1; + SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; + if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { + throw default_exception("Overflow encountered when expanding vector"); + } + SZ *mem, *old_mem = reinterpret_cast(m_data) - 2; +#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5 + if (__has_trivial_copy(T)) { +#else + if (std::is_trivially_copyable::value) { +#endif + mem = (SZ*)memory::reallocate(old_mem, new_capacity_T); + m_data = reinterpret_cast(mem + 2); + } else { + mem = (SZ*)memory::allocate(new_capacity_T); + auto old_data = m_data; + auto old_size = size(); + mem[1] = old_size; + m_data = reinterpret_cast(mem + 2); + for (unsigned i = 0; i < old_size; ++i) { + new (&m_data[i]) T(std::move(old_data[i])); + old_data[i].~T(); + } + memory::deallocate(old_mem); + } + *mem = new_capacity; + } + } + + void copy_core(vector const & source) { + SZ size = source.size(); + SZ capacity = source.capacity(); + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); + *mem = capacity; + mem++; + *mem = size; + mem++; + m_data = reinterpret_cast(mem); + const_iterator it = source.begin(); + iterator it2 = begin(); + SASSERT(it2 == m_data); + const_iterator e = source.end(); + for (; it != e; ++it, ++it2) { + new (it2) T(*it); + } + } + + void destroy() { + if (m_data) { + if (CallDestructors) { + destroy_elements(); + } + free_memory(); + } + } + +public: + typedef T data; + typedef T * iterator; + typedef const T * const_iterator; + + vector(): + m_data(nullptr) { + } + + vector(SZ s) { + if (s == 0) { + m_data = nullptr; + return; + } + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2)); + *mem = s; + mem++; + *mem = s; + mem++; + m_data = reinterpret_cast(mem); + // initialize elements + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + new (it) T(); + } + } + + vector(SZ s, T const & elem): + m_data(nullptr) { + resize(s, elem); + } + + vector(vector const & source): + m_data(nullptr) { + if (source.m_data) { + copy_core(source); + } + SASSERT(size() == source.size()); + } + + vector(vector&& other) : m_data(nullptr) { + std::swap(m_data, other.m_data); + } + + vector(SZ s, T const * data): + m_data(nullptr) { + for (SZ i = 0; i < s; i++) { + push_back(data[i]); + } + } + + + ~vector() { + destroy(); + } + + 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 true; + } + + 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); + } + else { + m_data = nullptr; + } + return *this; + } + + vector & operator=(vector && source) { + if (this == &source) { + return *this; + } + destroy(); + m_data = nullptr; + 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(); + } + reinterpret_cast(m_data)[SIZE_IDX] = 0; + } + } + + void clear() { reset(); } + + bool empty() const { + return m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == 0; + } + + SZ size() const { + if (m_data == nullptr) { + return 0; + } + return reinterpret_cast(m_data)[SIZE_IDX]; + } + + SZ capacity() const { + if (m_data == nullptr) { + return 0; + } + return reinterpret_cast(m_data)[CAPACITY_IDX]; + } + + 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(); + } + } + reinterpret_cast(m_data)[SIZE_IDX] = 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(); + } + reinterpret_cast(m_data)[SIZE_IDX]--; + } + + vector& push_back(T const & elem) { + if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { + expand_vector(); + } + new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); + reinterpret_cast(m_data)[SIZE_IDX]++; + return *this; + } + + template + vector& push_back(T const& elem, T elem2, Args ... elems) { + push_back(elem); + push_back(elem2, elems ...); + return *this; + } + + vector& push_back(T && elem) { + if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { + expand_vector(); + } + new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); + reinterpret_cast(m_data)[SIZE_IDX]++; + return *this; + } + + void insert(T const & elem) { + push_back(elem); + } + + void erase(iterator pos) { + SASSERT(pos >= begin() && pos < end()); + iterator prev = pos; + ++pos; + iterator e = end(); + for(; pos != e; ++pos, ++prev) { + *prev = *pos; + } + reinterpret_cast(m_data)[SIZE_IDX]--; + } + + void erase(T const & elem) { + iterator it = std::find(begin(), end(), elem); + if (it != end()) { + erase(it); + } + } + + void shrink(SZ s) { + if (m_data) { + SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); + if (CallDestructors) { + iterator it = m_data + s; + iterator e = end(); + for(; it != e; ++it) { + it->~T(); + } + } + reinterpret_cast(m_data)[SIZE_IDX] = s; + } + else { + SASSERT(s == 0); + } + } + + template + void resize(SZ s, Args args...) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + reinterpret_cast(m_data)[SIZE_IDX] = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(std::forward(args)); + } + } + + void resize(SZ s) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + reinterpret_cast(m_data)[SIZE_IDX] = 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(SZ sz, T const * data) { + for(SZ i = 0; i < sz; ++i) { + push_back(data[i]); + } + } + + T * c_ptr() const { + return m_data; + } + + void swap(vector & other) { + 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); + } +}; + +template +class ptr_vector : public vector { +public: + ptr_vector():vector() {} + ptr_vector(unsigned s):vector(s) {} + ptr_vector(unsigned s, T * elem):vector(s, elem) {} + ptr_vector(ptr_vector const & source):vector(source) {} + ptr_vector(ptr_vector && other) : vector(std::move(other)) {} + ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {} + ptr_vector & operator=(ptr_vector const & source) { + vector::operator=(source); + return *this; + } +}; template -using svector = old_svector; +class svector : public vector { +public: + svector():vector() {} + svector(SZ s):vector(s) {} + svector(SZ s, T const & elem):vector(s, elem) {} + svector(svector const & source):vector(source) {} + svector(svector && other) : vector(std::move(other)) {} + svector(SZ s, T const * data):vector(s, data) {} + svector & operator=(svector const & source) { + vector::operator=(source); + return *this; + } +}; + + + +using int_vector = svector; +using unsigned_vector = svector; +using char_vector = svector; +using signed_char_vector = svector; +using double_vector = svector; +using bool_vector = svector; template -using ptr_vector = old_ptr_vector; - -using int_vector = old_svector; -using unsigned_vector = old_svector; -using char_vector = old_svector; -using signed_char_vector = old_svector; -using double_vector = old_svector; -using bool_vector = old_svector; - -template -inline std::ostream& operator<<(std::ostream& out, old_svector const& v) { +inline std::ostream& operator<<(std::ostream& out, svector const& v) { for (unsigned u : v) out << u << " "; return out; }