mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-23 18:44:02 +00:00
Code Activity

[WIP] Update code base to use std::span (#8269)

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-21 12:42:19 -08:00 • committed by GitHub
parent 1bb471447e
commit 7686e861a8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 192 additions and 106 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/test/bits.cpp
View file

@ -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";

136
src/util/bit_util.cpp
View file

@ -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];

116
src/util/bit_util.h
View file

@ -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));
}

8
src/util/hash.h
View file

@ -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>

18
src/util/ref_vector.h
View file

@ -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 {