mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-23 16:57:51 +00:00
Code Activity

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

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-21 19:54:53 -08:00 • committed by Nikolaj Bjorner
parent 3097f7f831
commit d4046253d5
5 changed files with 89 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/ref_buffer.h
View file

@ -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) {
for (unsigned i = 0; i < n; ++i) {
push_back(elems[i]);
void append(std::span<T * const> elems) {
for (auto elem : elems) {
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());
}