From 725c0933ad7a7bc42a1c0c9e866b15b7e83786aa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Jun 2025 09:04:47 -0700
Subject: [PATCH] use usize to work around mess with static_cast<unsigned>
 insertions when looping over small vectors

---
 src/util/vector.h | 553 +---------------------------------------------
 1 file changed, 2 insertions(+), 551 deletions(-)

diff --git a/src/util/vector.h b/src/util/vector.h
index 67f6218ed..f3bd5da6b 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -45,556 +45,8 @@ Revision History:
 template <typename T>
 using std_vector = std::vector<T, std_allocator<T>>;
 
-#if 0
-
-template<typename T, bool CallDestructors = true, typename SZ = unsigned>
-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<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();
-        }
-    }
-
-public:
-    typedef T data_t;
-    typedef T* iterator;
-    typedef const T* const_iterator;
-
-    vector() = default;
-
-    vector(SZ s) {
-        init(s);
-    }
-
-    void init(SZ s) {
-        SASSERT(m_data == nullptr);
-        if (s == 0) {
-            return;
-        }
-        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();
-        }
-    }
-
-    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]);
-        }
-    }
-
-
-    ~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);
-        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;
-        }
-    };
-
-    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
+template <typename T>
+inline unsigned usize(std_vector<T> const& v) { return static_cast<unsigned>(v.size()); }
 
 template<typename T, bool CallDestructors=true, typename SZ = unsigned>
 class vector {
@@ -1163,7 +615,6 @@ public:
 
 };
 
-#endif
 
 template<typename T>
 class ptr_vector : public vector<T *, false> {