From b0313ca80ab7dc4f87ee82326a2b7cf1cc77b533 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 21 Jan 2026 19:54:53 -0800 Subject: [PATCH] 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 | 37 ++++++++++++++++++++++++++++--------- src/util/buffer.h | 23 +++++++++++++++++------ src/util/permutation.h | 35 ++++++++++++++++++++++++++--------- src/util/ref_buffer.h | 12 +++++++++--- src/util/util.h | 11 +++++++++-- 5 files changed, 89 insertions(+), 29 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index f92b51e6b..dfdad9e0f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -48,6 +48,7 @@ Revision History: #include "util/dependency.h" #include "util/rlimit.h" #include +#include #define RECYCLE_FREE_AST_INDICES @@ -1667,17 +1668,29 @@ public: } template - void inc_array_ref(unsigned sz, T * const * a) { - for(unsigned i = 0; i < sz; ++i) { - inc_ref(a[i]); + void inc_array_ref(std::span a) { + for(auto elem : a) { + inc_ref(elem); } } + // Backward compatibility overload + template + void inc_array_ref(unsigned sz, T * const * a) { + inc_array_ref(std::span(a, sz)); + } + + template + void dec_array_ref(std::span a) { + for(auto elem : a) { + dec_ref(elem); + } + } + + // Backward compatibility overload template void dec_array_ref(unsigned sz, T * const * a) { - for(unsigned i = 0; i < sz; ++i) { - dec_ref(a[i]); - } + dec_array_ref(std::span(a, sz)); } static unsigned get_node_size(ast const * n); @@ -2405,11 +2418,17 @@ private: } template - void push_dec_array_ref(unsigned sz, T * const * a) { - for(unsigned i = 0; i < sz; ++i) { - push_dec_ref(a[i]); + void push_dec_array_ref(std::span a) { + for(auto elem : a) { + push_dec_ref(elem); } } + + // Backward compatibility overload + template + void push_dec_array_ref(unsigned sz, T * const * a) { + push_dec_array_ref(std::span(a, sz)); + } }; typedef ast_manager::expr_array expr_array; diff --git a/src/util/buffer.h b/src/util/buffer.h index c36aa03bb..6700e617c 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -22,6 +22,7 @@ Revision History: #pragma once #include +#include #include "util/memory_manager.h" template @@ -192,12 +193,17 @@ public: return m_buffer; } - void append(unsigned n, T const * elems) { - for (unsigned i = 0; i < n; ++i) { - push_back(elems[i]); + void append(std::span elems) { + for (auto const& elem : elems) { + push_back(elem); } } + // Backward compatibility overload + void append(unsigned n, T const * elems) { + append(std::span(elems, n)); + } + void append(const buffer& source) { append(source.size(), source.data()); } @@ -265,11 +271,16 @@ public: template class ptr_buffer : public buffer { public: - void append(unsigned n, T * const * elems) { - for (unsigned i = 0; i < n; ++i) { - this->push_back(elems[i]); + void append(std::span elems) { + for (auto elem : elems) { + this->push_back(elem); } } + + // Backward compatibility overload + void append(unsigned n, T * const * elems) { + append(std::span(elems, n)); + } }; template diff --git a/src/util/permutation.h b/src/util/permutation.h index f48872e5c..fd623f127 100644 --- a/src/util/permutation.h +++ b/src/util/permutation.h @@ -18,7 +18,8 @@ Revision History: --*/ #pragma once -#include +#include +#include #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 -void apply_permutation_core(unsigned sz, T * data, unsigned * p) { - int * p1 = reinterpret_cast(p); - for (int i = 0; i < static_cast(sz); ++i) { +void apply_permutation_core(std::span data, std::span p) { + SASSERT(data.size() == p.size()); + int * p1 = reinterpret_cast(p.data()); + int sz = static_cast(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(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 +void apply_permutation_core(unsigned sz, T * data, unsigned * p) { + apply_permutation_core(std::span(data, sz), std::span(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 -void apply_permutation(unsigned sz, T * data, unsigned const * p) { - apply_permutation_core(sz, data, const_cast(p)); +void apply_permutation(std::span data, std::span p) { + SASSERT(data.size() == p.size()); + apply_permutation_core(data, std::span(const_cast(p.data()), p.size())); // restore p - int * p1 = reinterpret_cast(const_cast(p)); - for (unsigned i = 0; i < sz; ++i) { + int * p1 = reinterpret_cast(const_cast(p.data())); + int sz = static_cast(p.size()); + for (int i = 0; i < sz; ++i) { p1[i] = - p1[i] - 1; } } +// Backward compatibility overload +template +void apply_permutation(unsigned sz, T * data, unsigned const * p) { + apply_permutation(std::span(data, sz), std::span(p, sz)); +} + diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h index 67b53c323..d82b0bd53 100644 --- a/src/util/ref_buffer.h +++ b/src/util/ref_buffer.h @@ -18,6 +18,7 @@ Revision History: --*/ #pragma once +#include #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) { - for (unsigned i = 0; i < n; ++i) { - push_back(elems[i]); + void append(std::span elems) { + for (auto elem : elems) { + push_back(elem); } } + // Backward compatibility overload + void append(unsigned n, T * const * elems) { + append(std::span(elems, n)); + } + void append(ref_buffer_core const & other) { append(other.size(), other.data()); } diff --git a/src/util/util.h b/src/util/util.h index e6fe1fd85..876605b72 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -28,6 +28,7 @@ Revision History: #include #include #include +#include #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -360,14 +361,20 @@ public: }; template -void shuffle(unsigned sz, T * array, random_gen & gen) { - int n = sz; +void shuffle(std::span array, random_gen & gen) { + int n = array.size(); while (--n > 0) { int k = gen() % (n + 1); std::swap(array[n], array[k]); } } +// Backward compatibility overload +template +void shuffle(unsigned sz, T * array, random_gen & gen) { + shuffle(std::span(array, sz), gen); +} + void fatal_error(int error_code); void set_fatal_error_handler(void (*pfn)(int error_code));