From 770c79a939c9eab3aec4f8a6112ed398867d4fc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Apr 2021 09:24:16 -0700 Subject: [PATCH] prepare for std::vector --- src/math/dd/dd_pdd.cpp | 8 +- src/math/hilbert/hilbert_basis.h | 2 +- src/math/polynomial/polynomial.cpp | 4 +- src/math/polynomial/upolynomial.cpp | 4 +- src/util/heap.h | 6 +- src/util/mpff.h | 2 +- src/util/mpfx.cpp | 4 +- src/util/mpfx.h | 4 +- src/util/ref_vector.h | 14 ++-- src/util/scoped_numeral_vector.h | 2 +- src/util/uint_set.h | 18 ++--- src/util/vector.h | 111 ++++++++++++++++++++++++++++ 12 files changed, 146 insertions(+), 33 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 2422f3fd1..0dbf3c6f9 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -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; } diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h index 46563195c..1bd87d60c 100644 --- a/src/math/hilbert/hilbert_basis.h +++ b/src/math/hilbert/hilbert_basis.h @@ -89,7 +89,7 @@ class hilbert_basis { reslimit& m_limit; 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 m_basis; // vector of current basis svector m_free_list; // free list of unused storage svector m_active; // active set diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 96e92f8ac..b85ac1cf5 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -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; } diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index fd4010453..ac0aec8ef 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -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 << ""; else tout << fr.m_parent_idx; diff --git a/src/util/heap.h b/src/util/heap.h index 7a348aa4d..df67b31be 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -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 { diff --git a/src/util/mpff.h b/src/util/mpff.h index f766236f8..c9012a2d0 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -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; diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index 98d05f66d..ff6db740a 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -258,7 +258,7 @@ void mpfx_manager::set_core(mpfx & n, mpz_manager & 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 & 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); diff --git a/src/util/mpfx.h b/src/util/mpfx.h index 0834995a9..7f34e7dc1 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -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; diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index 27d6e7e3a..9e502335e 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -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(); diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index f53d93470..b586b5181 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -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)); } diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 3f0d45856..2b7e36360 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -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(); } diff --git a/src/util/vector.h b/src/util/vector.h index 1a64a7cae..c6981d362 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -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 +// +// template +// struct memory_allocator { +// typedef T value_type; +// etc (interface seems to change between C++17, 20 versions) +// }; +// + +#include + +template +class vector : public std::vector { +public: + typedef T data_t; + typedef typename std::vector::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 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 class vector { #define SIZE_IDX -1 @@ -602,6 +711,8 @@ public: }; +#endif + template class ptr_vector : public vector { public: