From 7686e861a830a381cc2350ecacb6bebc27d53b1b Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 21 Jan 2026 12:42:19 -0800
Subject: [PATCH] [WIP] Update code base to use std::span (#8269)

* Initial plan

* Add std::span to bit_util.h with backward compatibility

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add std::span to hash.h unsigned_ptr_hash function

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add std::span to ref_vector.h append and constructor

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/test/bits.cpp     |  20 +++----
 src/util/bit_util.cpp | 136 +++++++++++++++++++++++-------------------
 src/util/bit_util.h   | 116 +++++++++++++++++++++++++----------
 src/util/hash.h       |   8 ++-
 src/util/ref_vector.h |  18 +++++-
 5 files changed, 192 insertions(+), 106 deletions(-)

diff --git a/src/test/bits.cpp b/src/test/bits.cpp
index e80d67c53..41295b184 100644
--- a/src/test/bits.cpp
+++ b/src/test/bits.cpp
@@ -27,17 +27,17 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k,
     for (unsigned sz = 1; sz <= dst_sz; ++sz) {
         if (trace)
             std::cout << "  for sz = " << sz << std::endl;
-        shl(src_sz, src, k, sz, actual_dst.data());
-        ENSURE(!has_one_at_first_k_bits(sz, actual_dst.data(), k));
+        shl(std::span<unsigned const>(src, src_sz), k, std::span<unsigned>(actual_dst.data(), sz));
+        ENSURE(!has_one_at_first_k_bits(std::span<unsigned const>(actual_dst.data(), sz), k));
         for (unsigned i = 0; i < sz; ++i) {
             if (trace && dst[i] != actual_dst[i])
                 std::cout << "UNEXPECTED RESULT at [" << i << "]: " << actual_dst[i] << ", expected: " << dst[i] << "\n";
             ENSURE(dst[i] == actual_dst[i]);
         }
         if (sz == src_sz) {
-            unsigned nz1 = nlz(sz, src);
-            if (nz1 >= k && !is_zero(sz, src)) {
-                unsigned nz2 = nlz(sz, actual_dst.data());
+            unsigned nz1 = nlz(std::span<unsigned const>(src, sz));
+            if (nz1 >= k && !is_zero(std::span<unsigned const>(src, sz))) {
+                unsigned nz2 = nlz(std::span<unsigned const>(actual_dst.data(), sz));
                 if (nz1 - k != nz2) {
                     if (trace)
                         std::cout << "nlz BUG, nlz1: " << nz1 << ", k: " << k << ", nlz2: " << nz2 << std::endl;
@@ -48,7 +48,7 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k,
         if (sz >= src_sz + (k/32) + 1) {
             svector<unsigned> new_src;
             new_src.resize(sz, 0xAAAAAAAA);
-            shr(sz, actual_dst.data(), k, new_src.data());
+            shr(std::span<unsigned const>(actual_dst.data(), sz), k, std::span<unsigned>(new_src.data(), sz));
             for (unsigned i = 0; i < src_sz; ++i) {
                 if (trace && src[i] != new_src[i]) {
                     std::cout << "shr BUG, inverting shl, at bit[" << i << "], " << new_src[i] << ", expected: " << src[i] << std::endl;
@@ -59,9 +59,9 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k,
     }
     if (trace)
         std::cout << "  shift by 1, k times" << std::endl;
-    copy(src_sz, src, dst_sz, actual_dst.data());
+    copy(std::span<unsigned const>(src, src_sz), std::span<unsigned>(actual_dst.data(), dst_sz));
     for (unsigned i = 0; i < k; ++i) {
-        shl(dst_sz, actual_dst.data(), 1, dst_sz, actual_dst.data());
+        shl(std::span<unsigned const>(actual_dst.data(), dst_sz), 1, std::span<unsigned>(actual_dst.data(), dst_sz));
     }
     for (unsigned i = 0; i < dst_sz; ++i) {
         if (trace && dst[i] != actual_dst[i])
@@ -71,7 +71,7 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k,
     if (src_sz <= dst_sz) {
         if (trace)
             std::cout << "  self-shl" << std::endl;
-        shl(src_sz, src, k, src_sz, const_cast<unsigned*>(src));
+        shl(std::span<unsigned const>(src, src_sz), k, std::span<unsigned>(const_cast<unsigned*>(src), src_sz));
         for (unsigned i = 0; i < src_sz; ++i) {
             if (trace && src[i] != dst[i])
                 std::cout << "UNEXPECTED RESULT at [" << i << "]: " << src[i] << ", expected: " << dst[i] << "\n";
@@ -131,7 +131,7 @@ static void tst_shr(unsigned src_sz, unsigned const * src, unsigned k,
     }
     svector<unsigned> actual_dst;
     actual_dst.resize(src_sz, 0xAAAAAAAA);
-    shr(src_sz, src, k, actual_dst.data());
+    shr(std::span<unsigned const>(src, src_sz), k, std::span<unsigned>(actual_dst.data(), src_sz));
     for (unsigned i = 0; i < src_sz; ++i) {
         if (trace && dst[i] != actual_dst[i])
             std::cout << "UNEXPECTED RESULT at [" << i << "]: " << actual_dst[i] << ", expected: " << dst[i] << "\n";
diff --git a/src/util/bit_util.cpp b/src/util/bit_util.cpp
index 960288177..a0c9705e9 100644
--- a/src/util/bit_util.cpp
+++ b/src/util/bit_util.cpp
@@ -78,9 +78,9 @@ unsigned nlz_core(unsigned x) {
 /**
    \brief Return the number of leading zero bits in data (a number of sz words).
 */
-unsigned nlz(unsigned sz, unsigned const * data) {
+unsigned nlz(std::span<unsigned const> data) {
     unsigned r = 0;
-    unsigned i = sz;
+    unsigned i = data.size();
     while (i > 0) {
         --i;
         unsigned d = data[i];
@@ -111,9 +111,9 @@ unsigned ntz_core(unsigned x) {
 /**
    \brief Return the number of trailing zero bits in data (a number of sz words).
 */
-unsigned ntz(unsigned sz, unsigned const * data) {
+unsigned ntz(std::span<unsigned const> data) {
     unsigned r = 0;
-    for (unsigned i = 0; i < sz; ++i) {
+    for (unsigned i = 0; i < data.size(); ++i) {
         unsigned d = data[i];
         if (d == 0)
             r += 32;
@@ -126,11 +126,12 @@ unsigned ntz(unsigned sz, unsigned const * data) {
 /**
    \brief dst <- src
    
-   Truncate if src_sz > dst_sz.
-   Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz.
+   Truncate if src.size() > dst.size().
+   Fill range [src.size(), dst.size()) of dst with zeros if dst.size() > src.size().
 */
-void copy(unsigned src_sz, unsigned const * src, 
-          unsigned dst_sz, unsigned * dst) {
+void copy(std::span<unsigned const> src, std::span<unsigned> dst) {
+    unsigned src_sz = src.size();
+    unsigned dst_sz = dst.size();
     if (dst_sz >= src_sz) {
         unsigned i;
         for (i = 0; i < src_sz; ++i) 
@@ -148,8 +149,8 @@ void copy(unsigned src_sz, unsigned const * src,
 /**
    \brief Return true if all words of data are zero.
 */
-bool is_zero(unsigned sz, unsigned const * data) {
-    for (unsigned i = 0; i < sz; ++i) 
+bool is_zero(std::span<unsigned const> data) {
+    for (unsigned i = 0; i < data.size(); ++i) 
         if (data[i])
             return false;
     return true;
@@ -158,21 +159,22 @@ bool is_zero(unsigned sz, unsigned const * data) {
 /**
    \brief Set all words of data to zero.
 */
-void reset(unsigned sz, unsigned * data) {
-    for (unsigned i = 0; i < sz; ++i)
+void reset(std::span<unsigned> data) {
+    for (unsigned i = 0; i < data.size(); ++i)
         data[i] = 0;
 }
 
 /**
    \brief dst <- src << k
    Store in dst the result of shifting src k bits to the left.
-   The result is truncated by dst_sz.
+   The result is truncated by dst.size().
 
-   \pre src_sz != 0
-   \pre dst_sz != 0
+   \pre !src.empty()
+   \pre !dst.empty()
 */
-void shl(unsigned src_sz, unsigned const * src, unsigned k, 
-         unsigned dst_sz, unsigned * dst) {
+void shl(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst) {
+    unsigned src_sz = src.size();
+    unsigned dst_sz = dst.size();
     SASSERT(src_sz != 0);
     SASSERT(dst_sz != 0);
     SASSERT(k != 0);
@@ -235,57 +237,64 @@ void shl(unsigned src_sz, unsigned const * src, unsigned k,
    \brief dst <- src >> k
    Store in dst the result of shifting src k bits to the right.
 
-   \pre dst must have size sz.
-   \pre src_sz != 0
-   \pre dst_sz != 0
+   \pre dst.size() == src.size() or both sizes can differ (handled generically)
+   \pre !src.empty()
+   \pre !dst.empty()
 */
-void shr(unsigned sz, unsigned const * src, unsigned k, unsigned * dst) {
-    unsigned digit_shift = k / (8 * sizeof(unsigned));
-    if (digit_shift >= sz) {
-        reset(sz, dst);
-        return;
-    }
-    unsigned bit_shift   = k % (8 * sizeof(unsigned));
-    unsigned comp_shift  = (8 * sizeof(unsigned)) - bit_shift;
-    unsigned new_sz      = sz - digit_shift;
-    if (new_sz < sz) {
-        unsigned i       = 0;
-        unsigned j       = digit_shift;
-        if (bit_shift != 0) {
-            for (; i < new_sz - 1; ++i, ++j) {
+void shr(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst) {
+    unsigned src_sz = src.size();
+    unsigned dst_sz = dst.size();
+    unsigned sz = src_sz;
+    
+    // Handle the case where src and dst have the same size (original first shr function)
+    if (src_sz == dst_sz) {
+        unsigned digit_shift = k / (8 * sizeof(unsigned));
+        if (digit_shift >= sz) {
+            reset(dst);
+            return;
+        }
+        unsigned bit_shift   = k % (8 * sizeof(unsigned));
+        unsigned comp_shift  = (8 * sizeof(unsigned)) - bit_shift;
+        unsigned new_sz      = sz - digit_shift;
+        if (new_sz < sz) {
+            unsigned i       = 0;
+            unsigned j       = digit_shift;
+            if (bit_shift != 0) {
+                for (; i < new_sz - 1; ++i, ++j) {
+                    dst[i] = src[j];
+                    dst[i] >>= bit_shift;
+                    dst[i] |= (src[j+1] << comp_shift);
+                }
                 dst[i] = src[j];
                 dst[i] >>= bit_shift;
-                dst[i] |= (src[j+1] << comp_shift);
             }
-            dst[i] = src[j];
-            dst[i] >>= bit_shift;
+            else {
+                for (; i < new_sz; ++i, ++j) {
+                    dst[i] = src[j];
+                }
+            }
+            for (unsigned i = new_sz; i < sz; ++i)
+                dst[i] = 0;
         }
         else {
-            for (; i < new_sz; ++i, ++j) {
-                dst[i] = src[j];
+            SASSERT(new_sz == sz);
+            SASSERT(bit_shift != 0);
+            unsigned i       = 0;
+            for (; i < new_sz - 1; ++i) {
+                dst[i] = src[i];
+                dst[i] >>= bit_shift;
+                dst[i] |= (src[i+1] << comp_shift);
             }
-        }
-        for (unsigned i = new_sz; i < sz; ++i)
-            dst[i] = 0;
-    }
-    else {
-        SASSERT(new_sz == sz);
-        SASSERT(bit_shift != 0);
-        unsigned i       = 0;
-        for (; i < new_sz - 1; ++i) {
             dst[i] = src[i];
             dst[i] >>= bit_shift;
-            dst[i] |= (src[i+1] << comp_shift);
         }
-        dst[i] = src[i];
-        dst[i] >>= bit_shift;
+        return;
     }
-}
-
-void shr(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, unsigned * dst) {
+    
+    // Handle the case where src and dst have different sizes (original second shr function)
     unsigned digit_shift = k / (8 * sizeof(unsigned));
     if (digit_shift >= src_sz) {
-        reset(dst_sz, dst);
+        reset(dst);
         return;
     }
     unsigned bit_shift   = k % (8 * sizeof(unsigned));
@@ -340,7 +349,8 @@ void shr(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, uns
 /**
    \brief Return true if one of the first k bits of src is not zero.
 */
-bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
+bool has_one_at_first_k_bits(std::span<unsigned const> data, unsigned k) {
+    unsigned sz = data.size();
     SASSERT(sz != 0);
     unsigned word_sz = k / (8 * sizeof(unsigned));
     if (word_sz > sz)
@@ -357,8 +367,8 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
     return false;
 }
 
-bool inc(unsigned sz, unsigned * data) {
-    for (unsigned i = 0; i < sz; ++i) {
+bool inc(std::span<unsigned> data) {
+    for (unsigned i = 0; i < data.size(); ++i) {
         data[i]++;
         if (data[i] != 0)
             return true; // no overflow
@@ -366,8 +376,8 @@ bool inc(unsigned sz, unsigned * data) {
     return false; // overflow
 }
 
-bool dec(unsigned sz, unsigned * data) {
-    for (unsigned i = 0; i < sz; ++i) {
+bool dec(std::span<unsigned> data) {
+    for (unsigned i = 0; i < data.size(); ++i) {
         data[i]--;
         if (data[i] != UINT_MAX)
             return true; // no underflow
@@ -375,7 +385,8 @@ bool dec(unsigned sz, unsigned * data) {
     return false; // underflow
 }
 
-bool lt(unsigned sz, unsigned * data1, unsigned * data2) {
+bool lt(std::span<unsigned> data1, std::span<unsigned> data2) {
+    unsigned sz = data1.size();
     unsigned i = sz;
     while (i > 0) {
         --i;
@@ -387,7 +398,8 @@ bool lt(unsigned sz, unsigned * data1, unsigned * data2) {
     return false;
 }
 
-bool add(unsigned sz, unsigned const * a, unsigned const * b, unsigned * c) {
+bool add(std::span<unsigned const> a, std::span<unsigned const> b, std::span<unsigned> c) {
+    unsigned sz = a.size();
     unsigned k = 0;
     for (unsigned j = 0; j < sz; ++j) {
         unsigned r = a[j] + b[j]; 
diff --git a/src/util/bit_util.h b/src/util/bit_util.h
index 8226bc7c9..33161f401 100644
--- a/src/util/bit_util.h
+++ b/src/util/bit_util.h
@@ -18,6 +18,8 @@ Revision History:
 --*/
 #pragma once
 
+#include <span>
+
 /**
    \brief Return the position of the most significant (set) bit of a
    nonzero unsigned integer.
@@ -32,7 +34,12 @@ unsigned nlz_core(unsigned x);
 /**
    \brief Return the number of leading zero bits in data (a number of sz words).
 */
-unsigned nlz(unsigned sz, unsigned const * data);
+unsigned nlz(std::span<unsigned const> data);
+
+// Backward compatibility overload
+inline unsigned nlz(unsigned sz, unsigned const * data) {
+    return nlz(std::span<unsigned const>(data, sz));
+}
 
 /**
    \brief Return the number of trailing zeros in a nonzero unsigned number.
@@ -42,62 +49,91 @@ unsigned ntz_core(unsigned x);
 /**
    \brief Return the number of trailing zero bits in data (a number of sz words).
 */
-unsigned ntz(unsigned sz, unsigned const * data);
+unsigned ntz(std::span<unsigned const> data);
+
+// Backward compatibility overload
+inline unsigned ntz(unsigned sz, unsigned const * data) {
+    return ntz(std::span<unsigned const>(data, sz));
+}
 
 /**
    \brief dst <- src
    
-   Truncate if src_sz > dst_sz.
-   Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz.
+   Truncate if src.size() > dst.size().
+   Fill range [src.size(), dst.size()) of dst with zeros if dst.size() > src.size().
 */
-void copy(unsigned src_sz, unsigned const * src, unsigned dst_sz, unsigned * dst);
+void copy(std::span<unsigned const> src, std::span<unsigned> dst);
+
+// Backward compatibility overload
+inline void copy(unsigned src_sz, unsigned const * src, unsigned dst_sz, unsigned * dst) {
+    copy(std::span<unsigned const>(src, src_sz), std::span<unsigned>(dst, dst_sz));
+}
 
 /**
    \brief Return true if all words of data are zero.
 */
-bool is_zero(unsigned sz, unsigned const * data);
+bool is_zero(std::span<unsigned const> data);
+
+// Backward compatibility overload
+inline bool is_zero(unsigned sz, unsigned const * data) {
+    return is_zero(std::span<unsigned const>(data, sz));
+}
 
 /**
    \brief Set all words of data to zero.
 */
-void reset(unsigned sz, unsigned * data);
+void reset(std::span<unsigned> data);
+
+// Backward compatibility overload
+inline void reset(unsigned sz, unsigned * data) {
+    reset(std::span<unsigned>(data, sz));
+}
 
 /**
    \brief dst <- src << k
    Store in dst the result of shifting src k bits to the left.
-   The result is truncated by dst_sz.
+   The result is truncated by dst.size().
 
-   \pre src_sz != 0
-   \pre dst_sz != 0
+   \pre !src.empty()
+   \pre !dst.empty()
 */
-void shl(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, unsigned * dst);
+void shl(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst);
+
+// Backward compatibility overload
+inline void shl(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, unsigned * dst) {
+    shl(std::span<unsigned const>(src, src_sz), k, std::span<unsigned>(dst, dst_sz));
+}
 
 /**
    \brief dst <- src >> k
    Store in dst the result of shifting src k bits to the right.
 
-   \pre dst must have size sz.
-   \pre src_sz != 0
-   \pre dst_sz != 0
+   \pre dst.size() == src.size() or both sizes can differ (handled generically)
+   \pre !src.empty()
+   \pre !dst.empty()
 */
-void shr(unsigned sz, unsigned const * src, unsigned k, unsigned * dst);
+void shr(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst);
 
-/**
-   \brief dst <- src >> k
-   Store in dst the result of shifting src k bits to the right.
+// Backward compatibility overloads
+inline void shr(unsigned sz, unsigned const * src, unsigned k, unsigned * dst) {
+    shr(std::span<unsigned const>(src, sz), k, std::span<unsigned>(dst, sz));
+}
+
+inline void shr(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, unsigned * dst) {
+    shr(std::span<unsigned const>(src, src_sz), k, std::span<unsigned>(dst, dst_sz));
+}
 
-   Truncate if src_sz > dst_sz.
-   Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz.
 
-   \pre src_sz != 0
-   \pre dst_sz != 0
-*/
-void shr(unsigned src_sz, unsigned const * src, unsigned k, unsigned dst_sz, unsigned * dst);
 
 /**
    \brief Return true if one of the first k bits of src is not zero.
 */
-bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k);
+bool has_one_at_first_k_bits(std::span<unsigned const> data, unsigned k);
+
+// Backward compatibility overload
+inline bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
+    return has_one_at_first_k_bits(std::span<unsigned const>(data, sz), k);
+}
 
 
 /**
@@ -105,26 +141,46 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k);
    
    Return true if no overflow occurred.
 */
-bool inc(unsigned sz, unsigned * data);
+bool inc(std::span<unsigned> data);
+
+// Backward compatibility overload
+inline bool inc(unsigned sz, unsigned * data) {
+    return inc(std::span<unsigned>(data, sz));
+}
 
 /**
    \brief data <- data - 1
    
    Return true if no underflow occurred.
 */
-bool dec(unsigned sz, unsigned * data);
+bool dec(std::span<unsigned> data);
+
+// Backward compatibility overload
+inline bool dec(unsigned sz, unsigned * data) {
+    return dec(std::span<unsigned>(data, sz));
+}
 
 /**
    \brief Return true if data1 < data2. 
 
    Both must have the same size.
 */
-bool lt(unsigned sz, unsigned * data1, unsigned * data2);
+bool lt(std::span<unsigned> data1, std::span<unsigned> data2);
+
+// Backward compatibility overload
+inline bool lt(unsigned sz, unsigned * data1, unsigned * data2) {
+    return lt(std::span<unsigned>(data1, sz), std::span<unsigned>(data2, sz));
+}
 
 
 /**
-   \brief Store in c the a+b. This procedure assumes that a,b,c are vectors of size sz.
+   \brief Store in c the a+b. This procedure assumes that a,b,c are vectors of the same size.
    Return false if a+b overflows.
 */
-bool add(unsigned sz, unsigned const * a, unsigned const * b, unsigned * c);
+bool add(std::span<unsigned const> a, std::span<unsigned const> b, std::span<unsigned> c);
+
+// Backward compatibility overload
+inline bool add(unsigned sz, unsigned const * a, unsigned const * b, unsigned * c) {
+    return add(std::span<unsigned const>(a, sz), std::span<unsigned const>(b, sz), std::span<unsigned>(c, sz));
+}
 
diff --git a/src/util/hash.h b/src/util/hash.h
index 20f7936e1..a8d63f0d6 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -20,6 +20,7 @@ Revision History:
 
 #include<algorithm>
 #include<string_view>
+#include<span>
 #include "util/util.h"
 
 #define mix(a,b,c)              \
@@ -68,8 +69,13 @@ inline unsigned hash_u_u(unsigned a, unsigned b) {
 
 unsigned string_hash(std::string_view str, unsigned init_value);
 
+inline unsigned unsigned_ptr_hash(std::span<unsigned const> vec, unsigned init_value) {
+    return string_hash(std::string_view(reinterpret_cast<char const*>(vec.data()), vec.size() * sizeof(unsigned)), init_value);
+}
+
+// Backward compatibility overload
 inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
-    return string_hash(std::string_view((char const*)(vec), len*4), init_value);
+    return unsigned_ptr_hash(std::span<unsigned const>(vec, len), init_value);
 }
 
 template<typename Composite, typename GetKindHashProc, typename GetChildHashProc>
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index c8d685ec7..f8bd4061b 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include<span>
 #include "util/vector.h"
 #include "util/obj_ref.h"
 #include "util/ref.h"
@@ -192,9 +193,14 @@ public:
             push_back(other[i]);
     }
 
+    void append(std::span<T * const> data) {
+        for(auto elem : data)
+            push_back(elem);
+    }
+
+    // Backward compatibility overload
     void append(unsigned sz, T * const * data) {
-        for(unsigned i = 0; i < sz; ++i)
-            push_back(data[i]);
+        append(std::span<T * const>(data, sz));
     }
 
     void operator=(ref_vector_core && other) noexcept {
@@ -249,9 +255,15 @@ public:
 
     ref_vector(ref_vector &&) noexcept = default;
 
+    ref_vector(TManager & m, std::span<T * const> data):
+        super(ref_manager_wrapper<T, TManager>(m)) {
+        this->append(data);
+    }
+
+    // Backward compatibility overload
     ref_vector(TManager & m, unsigned sz, T * const * data):
         super(ref_manager_wrapper<T, TManager>(m)) {
-        this->append(sz, data);
+        this->append(std::span<T * const>(data, sz));
     }
     
     TManager & get_manager() const {