Extend std::span adoption to utility and AST functions (#8271)

* Initial plan

* Add std::span to utility functions (buffer, ref_buffer, permutation, util)

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

* Add std::span to ast_manager array ref functions

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

* Fix: Use consistent int loop variable in apply_permutation

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/ast/ast.h

@@ -48,6 +48,7 @@ Revision History:
 #include "util/dependency.h"
 #include "util/rlimit.h"
 #include <variant>
+#include <span>
 
 #define RECYCLE_FREE_AST_INDICES
 
@@ -1667,17 +1668,29 @@ public:
     }
 
     template<typename T>
-    void inc_array_ref(unsigned sz, T * const * a) {
+    void inc_array_ref(std::span<T * const> a) {
-        for(unsigned i = 0; i < sz; ++i) {
+        for(auto elem : a) {
-            inc_ref(a[i]);
+            inc_ref(elem);
         }
     }
 
+    // Backward compatibility overload
+    template<typename T>
+    void inc_array_ref(unsigned sz, T * const * a) {
+        inc_array_ref(std::span<T * const>(a, sz));
+    }
+
+    template<typename T>
+    void dec_array_ref(std::span<T * const> a) {
+        for(auto elem : a) {
+            dec_ref(elem);
+        }
+    }
+
+    // Backward compatibility overload
     template<typename T>
     void dec_array_ref(unsigned sz, T * const * a) {
-        for(unsigned i = 0; i < sz; ++i) {
+        dec_array_ref(std::span<T * const>(a, sz));
-            dec_ref(a[i]);
-        }
     }
 
     static unsigned get_node_size(ast const * n);
@@ -2405,11 +2418,17 @@ private:
     }
 
     template<typename T>
-    void push_dec_array_ref(unsigned sz, T * const * a) {
+    void push_dec_array_ref(std::span<T * const> a) {
-        for(unsigned i = 0; i < sz; ++i) {
+        for(auto elem : a) {
-            push_dec_ref(a[i]);
+            push_dec_ref(elem);
         }
     }
+
+    // Backward compatibility overload
+    template<typename T>
+    void push_dec_array_ref(unsigned sz, T * const * a) {
+        push_dec_array_ref(std::span<T * const>(a, sz));
+    }
 };
 
 typedef ast_manager::expr_array expr_array;

src/util/buffer.h

@@ -22,6 +22,7 @@ Revision History:
 #pragma once
 
 #include <cstddef>
+#include <span>
 #include "util/memory_manager.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
@@ -192,12 +193,17 @@ public:
         return m_buffer;
     }
 
-    void append(unsigned n, T const * elems) {
+    void append(std::span<T const> elems) {
-        for (unsigned i = 0; i < n; ++i) {
+        for (auto const& elem : elems) {
-            push_back(elems[i]);
+            push_back(elem);
         }
     }
 
+    // Backward compatibility overload
+    void append(unsigned n, T const * elems) {
+        append(std::span<T const>(elems, n));
+    }
+
     void append(const buffer& source) {
         append(source.size(), source.data());
     }
@@ -265,11 +271,16 @@ public:
 template<typename T, unsigned INITIAL_SIZE=16>
 class ptr_buffer : public buffer<T *, false, INITIAL_SIZE> {
 public:
-    void append(unsigned n, T * const * elems) {
+    void append(std::span<T * const> elems) {
-        for (unsigned i = 0; i < n; ++i) {
+        for (auto elem : elems) {
-            this->push_back(elems[i]);
+            this->push_back(elem);
         }
     }
+
+    // Backward compatibility overload
+    void append(unsigned n, T * const * elems) {
+        append(std::span<T * const>(elems, n));
+    }
 };
 
 template<typename T, unsigned INITIAL_SIZE=16>

src/util/permutation.h

@@ -18,7 +18,8 @@ Revision History:
 --*/
 #pragma once
 
-#include<ostream>
+#include <ostream>
+#include <span>
 #include "util/vector.h"
 
 class permutation {
@@ -55,9 +56,11 @@ inline std::ostream & operator<<(std::ostream & out, permutation const & p) {
    Use apply_permutation if p must not be preserved
 */
 template<typename T>
-void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
+void apply_permutation_core(std::span<T> data, std::span<unsigned> p) {
-    int * p1 = reinterpret_cast<int*>(p);
+    SASSERT(data.size() == p.size());
-    for (int i = 0; i < static_cast<int>(sz); ++i) {
+    int * p1 = reinterpret_cast<int*>(p.data());
+    int sz = static_cast<int>(data.size());
+    for (int i = 0; i < sz; ++i) {
         if (p1[i] < 0)
             continue; // already processed
         int j = i;
@@ -65,7 +68,7 @@ void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
             SASSERT(j >= 0);
             int p_j = p1[j];
             SASSERT(p_j >= 0);
-            SASSERT(p_j < static_cast<int>(sz));
+            SASSERT(p_j < sz);
             p1[j]   = - p1[j] - 1; // mark as done
             if (p_j == i)
                 break; // cycle starting at i is done
@@ -75,6 +78,12 @@ void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
     }
 }
 
+// Backward compatibility overload
+template<typename T>
+void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
+    apply_permutation_core(std::span<T>(data, sz), std::span<unsigned>(p, sz));
+}
+
 /**
    \brief Apply permutation p to data.
    The algorithm does not use any extra memory.
@@ -82,12 +91,20 @@ void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
    Requirement: swap(T, T) must be available.
 */
 template<typename T>
-void apply_permutation(unsigned sz, T * data, unsigned const * p) {
+void apply_permutation(std::span<T> data, std::span<unsigned const> p) {
-    apply_permutation_core(sz, data, const_cast<unsigned*>(p));
+    SASSERT(data.size() == p.size());
+    apply_permutation_core(data, std::span<unsigned>(const_cast<unsigned*>(p.data()), p.size()));
     // restore p
-    int * p1 = reinterpret_cast<int*>(const_cast<unsigned*>(p));
+    int * p1 = reinterpret_cast<int*>(const_cast<unsigned*>(p.data()));
-    for (unsigned i = 0; i < sz; ++i) { 
+    int sz = static_cast<int>(p.size());
+    for (int i = 0; i < sz; ++i) { 
         p1[i] = - p1[i] - 1;
     }
 }
 
+// Backward compatibility overload
+template<typename T>
+void apply_permutation(unsigned sz, T * data, unsigned const * p) {
+    apply_permutation(std::span<T>(data, sz), std::span<unsigned const>(p, sz));
+}
+

src/util/ref_buffer.h

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include <span>
 #include "util/buffer.h"
 #include "util/obj_ref.h"
 #include "util/ref_vector.h"
@@ -114,12 +115,17 @@ public:
         m_buffer.finalize();
     }        
 
-    void append(unsigned n, T * const * elems) {
+    void append(std::span<T * const> elems) {
-        for (unsigned i = 0; i < n; ++i) {
+        for (auto elem : elems) {
-            push_back(elems[i]);
+            push_back(elem);
         }
     }
 
+    // Backward compatibility overload
+    void append(unsigned n, T * const * elems) {
+        append(std::span<T * const>(elems, n));
+    }
+
     void append(ref_buffer_core const & other) {
         append(other.size(), other.data());
     }

src/util/util.h

@@ -28,6 +28,7 @@ Revision History:
 #include <functional>
 #include <algorithm>
 #include <iterator>
+#include <span>
 
 #ifndef SIZE_MAX
 #define SIZE_MAX std::numeric_limits<std::size_t>::max()
@@ -360,14 +361,20 @@ public:
 };
 
 template<typename T>
-void shuffle(unsigned sz, T * array, random_gen & gen) {
+void shuffle(std::span<T> array, random_gen & gen) {
-    int n = sz;
+    int n = array.size();
     while (--n > 0) {
         int k = gen() % (n + 1);
         std::swap(array[n], array[k]);
     }
 }
 
+// Backward compatibility overload
+template<typename T>
+void shuffle(unsigned sz, T * array, random_gen & gen) {
+    shuffle(std::span<T>(array, sz), gen);
+}
+
 void fatal_error(int error_code);
 
 void set_fatal_error_handler(void (*pfn)(int error_code));