mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
01a419546f
commit
a1bcf136a6
2 changed files with 527 additions and 92 deletions
|
|
@ -99,7 +99,6 @@ namespace smt {
|
|||
m_model_generator->set_context(this);
|
||||
}
|
||||
|
||||
::
|
||||
/**
|
||||
\brief retrieve flag for when cancelation is possible.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -45,120 +45,556 @@ Revision History:
|
|||
template <typename T>
|
||||
using std_vector = std::vector<T, std_allocator<T>>;
|
||||
|
||||
#if 0
|
||||
#if 1
|
||||
|
||||
// portability guide to std::vector.
|
||||
// memory allocator should be based on memory_allocator<T>
|
||||
//
|
||||
// template<typename T>
|
||||
// struct memory_allocator {
|
||||
// typedef T value_type;
|
||||
// etc (interface seems to change between C++17, 20 versions)
|
||||
// };
|
||||
//
|
||||
template<typename T, bool CallDestructors = true, typename SZ = unsigned>
|
||||
class vector {
|
||||
SZ m_capacity = 0;
|
||||
SZ m_size = 0;
|
||||
T* m_data = nullptr;
|
||||
|
||||
// Note:
|
||||
// polynomial.h contains declaration
|
||||
// typedef svector<numeral> 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.
|
||||
//
|
||||
void destroy_elements() {
|
||||
std::destroy_n(m_data, size());
|
||||
}
|
||||
|
||||
#include <vector>
|
||||
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<T*>(memory::allocate(sizeof(T) * m_capacity));
|
||||
}
|
||||
else {
|
||||
static_assert(std::is_nothrow_move_constructible<T>::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<T>::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<T*>(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<typename T, bool CallDestructors=true, typename SZ = unsigned>
|
||||
class vector : public std::vector<T> {
|
||||
public:
|
||||
typedef T data_t;
|
||||
typedef typename std::vector<T>::iterator iterator;
|
||||
typedef T* iterator;
|
||||
typedef const T* const_iterator;
|
||||
|
||||
vector() = default;
|
||||
|
||||
vector() {}
|
||||
vector(SZ s) {
|
||||
// TODO resize(s, T());
|
||||
}
|
||||
vector(SZ s, T const& e) {
|
||||
// TODO resize(s, e);
|
||||
init(s);
|
||||
}
|
||||
|
||||
vector(SZ s, T const* e) {
|
||||
// TODO
|
||||
}
|
||||
|
||||
void reset() { clear(); }
|
||||
void finalize() { clear(); }
|
||||
void reserve(SZ s, T const & d) {
|
||||
if (s > size())
|
||||
resize(s, d);
|
||||
}
|
||||
void reserve(SZ s) {
|
||||
|
||||
}
|
||||
|
||||
void setx(SZ idx, T const & elem, T const & d) {
|
||||
if (idx >= size())
|
||||
resize(idx+1, d);
|
||||
(*this)[idx] = elem;
|
||||
}
|
||||
|
||||
T const & get(SZ idx, T const & d) const {
|
||||
if (idx >= size()) {
|
||||
return d;
|
||||
void init(SZ s) {
|
||||
SASSERT(m_data == nullptr);
|
||||
if (s == 0) {
|
||||
return;
|
||||
}
|
||||
return (*this)[idx];
|
||||
}
|
||||
|
||||
void insert(T const & elem) {
|
||||
push_back(elem);
|
||||
}
|
||||
|
||||
void erase(iterator pos) {
|
||||
// TODO
|
||||
}
|
||||
|
||||
void erase(T const& e) {
|
||||
// TODO
|
||||
}
|
||||
void fill(T const & elem) {
|
||||
for (auto& e : *this)
|
||||
e = elem;
|
||||
}
|
||||
|
||||
void fill(unsigned sz, T const & elem) {
|
||||
resize(sz);
|
||||
fill(elem);
|
||||
}
|
||||
|
||||
void shrink(SZ s) {
|
||||
resize(s);
|
||||
}
|
||||
void reverse() {
|
||||
SZ sz = size();
|
||||
for (SZ i = 0; i < sz/2; ++i) {
|
||||
std::swap((*this)[i], (*this)[sz-i-1]);
|
||||
m_data = reinterpret_cast<T*>(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();
|
||||
}
|
||||
}
|
||||
|
||||
void append(vector<T, CallDestructors> const & other) {
|
||||
for(SZ i = 0; i < other.size(); ++i) {
|
||||
push_back(other[i]);
|
||||
vector(SZ s, T const& elem) {
|
||||
resize(s, elem);
|
||||
}
|
||||
|
||||
vector(vector const& source) {
|
||||
if (source.m_data) {
|
||||
copy_core(source);
|
||||
}
|
||||
SASSERT(size() == source.size());
|
||||
}
|
||||
|
||||
vector(vector&& other) noexcept {
|
||||
std::swap(m_data, other.m_data);
|
||||
}
|
||||
|
||||
vector(SZ s, T const* data) {
|
||||
for (SZ i = 0; i < s; i++) {
|
||||
push_back(data[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void append(unsigned n, T const* elems) {
|
||||
// TODO
|
||||
|
||||
~vector() {
|
||||
destroy();
|
||||
}
|
||||
|
||||
bool contains(T const & elem) const {
|
||||
for (auto const& e : *this)
|
||||
if (e == elem)
|
||||
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);
|
||||
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<bool(T)>& 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<bool(T)>& predicate) const {
|
||||
vector result;
|
||||
for (auto& t : *this)
|
||||
if (predicate(t))
|
||||
result.push_back(t);
|
||||
return result;
|
||||
}
|
||||
|
||||
vector& filter_update(std::function<bool(T)>& 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 <typename S>
|
||||
vector<S> map_pure(std::function<S(T)>& f) const {
|
||||
vector<S> result;
|
||||
for (auto& t : *this)
|
||||
result.push_back(f(t));
|
||||
return result;
|
||||
}
|
||||
|
||||
vector& map_update(std::function<T(T)>& 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<SZ>(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 <typename ...Args>
|
||||
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 || m_size == m_capacity) {
|
||||
expand_vector();
|
||||
}
|
||||
new (m_data + m_size) T(std::move(elem));
|
||||
++m_size;
|
||||
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 = std::move(*pos);
|
||||
}
|
||||
pop_back();
|
||||
}
|
||||
|
||||
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 <typename UnaryPredicate>
|
||||
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) {
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Args>
|
||||
void resize(SZ s, Args args...) {
|
||||
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(std::forward<Args>(args));
|
||||
}
|
||||
}
|
||||
|
||||
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<T, CallDestructors> 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]);
|
||||
}
|
||||
}
|
||||
|
||||
void init(vector<T, CallDestructors> 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue