mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 19:05:51 +00:00
prepare for std::vector
This commit is contained in:
Nikolaj Bjorner
parent
831afa8124
commit
770c79a939
12 changed files with 146 additions and 33 deletions
|
|
@ -1010,7 +1010,7 @@ namespace dd {
|
|||
m_todo.push_back(p);
|
||||
while (!m_todo.empty()) {
|
||||
PDD r = m_todo.back();
|
||||
if (is_marked(r))
|
||||
if (is_marked(r))
|
||||
m_todo.pop_back();
|
||||
else if (is_val(r))
|
||||
m_todo.pop_back();
|
||||
|
|
@ -1025,8 +1025,10 @@ namespace dd {
|
|||
max_d = std::max(d, max_d);
|
||||
m_todo.pop_back();
|
||||
}
|
||||
else
|
||||
m_todo.push_back(lo(r)).push_back(hi(r));
|
||||
else {
|
||||
m_todo.push_back(lo(r));
|
||||
m_todo.push_back(hi(r));
|
||||
}
|
||||
}
|
||||
return max_d;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ class hilbert_basis {
|
|||
reslimit& m_limit;
|
||||
vector<num_vector> m_ineqs; // set of asserted inequalities
|
||||
bool_vector m_iseq; // inequalities that are equalities
|
||||
num_vector m_store; // store of vectors
|
||||
mutable num_vector m_store; // store of vectors
|
||||
svector<offset_t> m_basis; // vector of current basis
|
||||
svector<offset_t> m_free_list; // free list of unused storage
|
||||
svector<offset_t> m_active; // active set
|
||||
|
|
|
|||
|
|
@ -4096,7 +4096,7 @@ namespace polynomial {
|
|||
// select a new random value in GF(p) that is not in vals, and store it in r
|
||||
void peek_fresh(scoped_numeral_vector const & vals, unsigned p, scoped_numeral & r) {
|
||||
SASSERT(vals.size() < p); // otherwise we can't keep the fresh value
|
||||
unsigned sz = vals.size();
|
||||
auto sz = vals.size();
|
||||
while (true) {
|
||||
m().set(r, rand() % p);
|
||||
// check if fresh value...
|
||||
|
|
@ -6240,7 +6240,7 @@ namespace polynomial {
|
|||
}
|
||||
|
||||
void reset() {
|
||||
unsigned sz = m_xs.size();
|
||||
auto sz = m_xs.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_max_degree[m_xs[i]] = 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2126,7 +2126,7 @@ namespace upolynomial {
|
|||
}
|
||||
frame_stack.push_back(drs_frame(parent_idx, sz, true));
|
||||
// right child
|
||||
translate(sz, p_stack.end() - sz, p_aux);
|
||||
translate(sz, p_stack.data() + p_stack.size() - sz, p_aux);
|
||||
normalize(p_aux);
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
p_stack.push_back(numeral());
|
||||
|
|
@ -2226,7 +2226,7 @@ namespace upolynomial {
|
|||
drs_frame & fr = frame_stack.back();
|
||||
unsigned sz = fr.m_size;
|
||||
SASSERT(sz <= p_stack.size());
|
||||
numeral const * p = p_stack.end() - sz;
|
||||
numeral const * p = p_stack.data() + p_stack.size() - sz;
|
||||
TRACE("upolynomial", tout << "processing frame #" << frame_stack.size() - 1 << "\n"
|
||||
<< "first: " << fr.m_first << ", left: " << fr.m_left << ", sz: " << fr.m_size << ", parent_idx: ";
|
||||
if (fr.m_parent_idx == UINT_MAX) tout << "<null>"; else tout << fr.m_parent_idx;
|
||||
|
|
|
|||
|
|
@ -139,7 +139,7 @@ public:
|
|||
if (empty()) {
|
||||
return;
|
||||
}
|
||||
memset(m_value2indices.begin(), 0, sizeof(int) * m_value2indices.size());
|
||||
memset(m_value2indices.data(), 0, sizeof(int) * m_value2indices.size());
|
||||
m_values.reset();
|
||||
m_values.push_back(-1);
|
||||
CASSERT("heap", check_invariant());
|
||||
|
|
@ -244,11 +244,11 @@ public:
|
|||
}
|
||||
|
||||
iterator begin() {
|
||||
return m_values.begin() + 1;
|
||||
return m_values.data() + 1;
|
||||
}
|
||||
|
||||
iterator end() {
|
||||
return m_values.end();
|
||||
return m_values.data() + m_values.size();
|
||||
}
|
||||
|
||||
const_iterator begin() const {
|
||||
|
|
|
|||
|
|
@ -112,7 +112,7 @@ class mpff_manager {
|
|||
|
||||
unsigned m_precision; //!< Number of words in the significand. Must be an even number.
|
||||
unsigned m_precision_bits; //!< Number of bits in the significand. Must be 32*m_precision.
|
||||
unsigned_vector m_significands; //!< Array containing all significands.
|
||||
mutable unsigned_vector m_significands; //!< Array containing all significands.
|
||||
unsigned m_capacity; //!< Number of significands that can be stored in m_significands.
|
||||
bool m_to_plus_inf; //!< If True, then round to plus infinity, otherwise to minus infinity
|
||||
id_gen m_id_gen;
|
||||
|
|
|
|||
|
|
@ -258,7 +258,7 @@ void mpfx_manager::set_core(mpfx & n, mpz_manager<SYNCH> & m, mpz const & v) {
|
|||
m_tmp_digits.reset();
|
||||
allocate_if_needed(n);
|
||||
n.m_sign = m.decompose(v, m_tmp_digits);
|
||||
unsigned sz = m_tmp_digits.size();
|
||||
auto sz = m_tmp_digits.size();
|
||||
if (sz > m_int_part_sz)
|
||||
throw overflow_exception();
|
||||
unsigned * w = words(n);
|
||||
|
|
@ -299,7 +299,7 @@ void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
|
|||
}
|
||||
m_tmp_digits.reset();
|
||||
m.decompose(tmp, m_tmp_digits);
|
||||
unsigned sz = m_tmp_digits.size();
|
||||
auto sz = m_tmp_digits.size();
|
||||
if (sz > m_total_sz)
|
||||
throw overflow_exception();
|
||||
unsigned * w = words(n);
|
||||
|
|
|
|||
|
|
@ -81,11 +81,11 @@ class mpfx_manager {
|
|||
unsigned m_int_part_sz;
|
||||
unsigned m_frac_part_sz;
|
||||
unsigned m_total_sz; //!< == m_int_part_sz + m_frac_part_sz
|
||||
unsigned_vector m_words; //!< Array containing all words
|
||||
mutable unsigned_vector m_words; //!< Array containing all words
|
||||
unsigned m_capacity; //!< Number of mpfx numerals that can be stored in m_words.
|
||||
bool m_to_plus_inf; //!< If True, then round to plus infinity, otherwise to minus infinity
|
||||
id_gen m_id_gen;
|
||||
unsigned_vector m_buffer0, m_buffer1, m_buffer2;
|
||||
mutable unsigned_vector m_buffer0, m_buffer1, m_buffer2;
|
||||
unsigned_vector m_tmp_digits;
|
||||
mpfx m_one;
|
||||
mpn_manager m_mpn_manager;
|
||||
|
|
|
|||
|
|
@ -58,28 +58,28 @@ public:
|
|||
ref_vector_core(ref_vector_core &&) noexcept = default;
|
||||
|
||||
~ref_vector_core() {
|
||||
dec_range_ref(m_nodes.begin(), m_nodes.end());
|
||||
dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
|
||||
}
|
||||
|
||||
void reset() {
|
||||
dec_range_ref(m_nodes.begin(), m_nodes.end());
|
||||
dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
|
||||
m_nodes.reset();
|
||||
}
|
||||
|
||||
void finalize() {
|
||||
dec_range_ref(m_nodes.begin(), m_nodes.end());
|
||||
dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
|
||||
m_nodes.finalize();
|
||||
}
|
||||
|
||||
void resize(unsigned sz) {
|
||||
if (sz < m_nodes.size())
|
||||
dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
|
||||
dec_range_ref(m_nodes.data() + sz, m_nodes.data() + m_nodes.size());
|
||||
m_nodes.resize(sz);
|
||||
}
|
||||
|
||||
void resize(unsigned sz, T * d) {
|
||||
if (sz < m_nodes.size()) {
|
||||
dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
|
||||
dec_range_ref(m_nodes.data() + sz, m_nodes.data() + m_nodes.size());
|
||||
m_nodes.shrink(sz);
|
||||
}
|
||||
else {
|
||||
|
|
@ -130,11 +130,11 @@ public:
|
|||
|
||||
T * get(unsigned idx, T * d) const { return m_nodes.get(idx, d); }
|
||||
|
||||
T * const * data() const { return m_nodes.begin(); }
|
||||
T * const * data() const { return m_nodes.data(); }
|
||||
|
||||
typedef T* const* iterator;
|
||||
|
||||
T ** data() { return m_nodes.begin(); }
|
||||
T ** data() { return m_nodes.data(); }
|
||||
|
||||
unsigned hash() const {
|
||||
unsigned sz = size();
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ public:
|
|||
}
|
||||
|
||||
void reset() {
|
||||
unsigned sz = this->size();
|
||||
auto sz = this->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m().del(this->operator[](i));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ public:
|
|||
|
||||
// Insert in the this object the elements in the set source.
|
||||
uint_set & operator |=(const uint_set & source) {
|
||||
unsigned source_size = source.size();
|
||||
auto source_size = source.size();
|
||||
if (source_size > size()) {
|
||||
resize(source_size + 1);
|
||||
}
|
||||
|
|
@ -91,7 +91,7 @@ public:
|
|||
}
|
||||
|
||||
uint_set& operator &=(const uint_set& source) {
|
||||
unsigned source_size = source.size();
|
||||
auto source_size = source.size();
|
||||
if (source_size < size()) {
|
||||
resize(source_size);
|
||||
}
|
||||
|
|
@ -102,7 +102,7 @@ public:
|
|||
}
|
||||
|
||||
bool operator==(const uint_set & source) const {
|
||||
unsigned min_size = size();
|
||||
auto min_size = size();
|
||||
if (source.size() < min_size) {
|
||||
min_size = source.size();
|
||||
}
|
||||
|
|
@ -111,12 +111,12 @@ public:
|
|||
return false;
|
||||
}
|
||||
}
|
||||
for (unsigned i = min_size; i < size(); ++i) {
|
||||
for (auto i = min_size; i < size(); ++i) {
|
||||
if ((*this)[i]) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
for (unsigned i = min_size; i < source.size(); ++i) {
|
||||
for (auto i = min_size; i < source.size(); ++i) {
|
||||
if (source[i]) {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -131,7 +131,7 @@ public:
|
|||
|
||||
// Return true if the this set is a subset of source.
|
||||
bool subset_of(const uint_set & source) const {
|
||||
unsigned min_size = size();
|
||||
auto min_size = size();
|
||||
if (source.size() < min_size) {
|
||||
min_size = source.size();
|
||||
}
|
||||
|
|
@ -140,7 +140,7 @@ public:
|
|||
return false;
|
||||
}
|
||||
}
|
||||
for (unsigned i = min_size; i < size(); ++i) {
|
||||
for (auto i = min_size; i < size(); ++i) {
|
||||
if ((*this)[i]) {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -252,7 +252,7 @@ public:
|
|||
void remove(unsigned v) {
|
||||
if (contains(v)) {
|
||||
m_in_set[v] = false;
|
||||
unsigned i = m_set.size();
|
||||
auto i = m_set.size();
|
||||
for (; i > 0 && m_set[--i] != v; )
|
||||
;
|
||||
SASSERT(m_set[i] == v);
|
||||
|
|
@ -282,7 +282,7 @@ public:
|
|||
iterator end() const { return m_set.end(); }
|
||||
// void reset() { m_set.reset(); m_in_set.reset(); }
|
||||
void reset() {
|
||||
unsigned sz = m_set.size();
|
||||
auto sz = m_set.size();
|
||||
for (unsigned i = 0; i < sz; ++i) m_in_set[m_set[i]] = false;
|
||||
m_set.reset();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,6 +40,115 @@ Revision History:
|
|||
#pragma warning(disable:4127)
|
||||
#endif
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
// 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)
|
||||
// };
|
||||
//
|
||||
|
||||
#include <vector>
|
||||
|
||||
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;
|
||||
|
||||
vector() {}
|
||||
vector(SZ s) {
|
||||
// resize(s, T());
|
||||
}
|
||||
vector(SZ s, T const& e) {
|
||||
// resize(s, e);
|
||||
}
|
||||
|
||||
vector(SZ s, T const* e) {
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
return (*this)[idx];
|
||||
}
|
||||
|
||||
void insert(T const & elem) {
|
||||
push_back(elem);
|
||||
}
|
||||
|
||||
void erase(iterator pos) {
|
||||
|
||||
}
|
||||
|
||||
void erase(T const& e) {
|
||||
|
||||
}
|
||||
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]);
|
||||
}
|
||||
}
|
||||
|
||||
void append(vector<T, CallDestructors> const & other) {
|
||||
for(SZ i = 0; i < other.size(); ++i) {
|
||||
push_back(other[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void append(unsigned n, T const* elems) {
|
||||
|
||||
}
|
||||
|
||||
bool contains(T const & elem) const {
|
||||
for (auto const& e : *this)
|
||||
if (e == elem)
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
#else
|
||||
|
||||
template<typename T, bool CallDestructors=true, typename SZ = unsigned>
|
||||
class vector {
|
||||
#define SIZE_IDX -1
|
||||
|
|
@ -602,6 +711,8 @@ public:
|
|||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
||||
template<typename T>
|
||||
class ptr_vector : public vector<T *, false> {
|
||||
public:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue