mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-26 10:05:38 +00:00
Code Activity

Add static linkage to inline functions in header files (#8519)

Browse source
This commit is contained in:
Copilot 2026-02-06 22:57:51 +00:00 • committed by GitHub
parent bee2b45743
commit 3095ab511f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/hash.h
View file

@ -36,7 +36,7 @@ Revision History:
c -= a; c -= b; c ^= (b>>15); \ c -= a; c -= b; c ^= (b>>15); \
} }
inline unsigned hash_u(unsigned a) { static inline unsigned hash_u(unsigned a) {
a = (a+0x7ed55d16) + (a<<12); a = (a+0x7ed55d16) + (a<<12);
a = (a^0xc761c23c) ^ (a>>19); a = (a^0xc761c23c) ^ (a>>19);
a = (a+0x165667b1) + (a<<5); a = (a+0x165667b1) + (a<<5);
@ -46,7 +46,7 @@ inline unsigned hash_u(unsigned a) {
return a; return a;
} }
inline unsigned hash_ull(unsigned long long a) { static inline unsigned hash_ull(unsigned long long a) {
a = (~a) + (a << 18); a = (~a) + (a << 18);
a ^= (a >> 31); a ^= (a >> 31);
a += (a << 2) + (a << 4); a += (a << 2) + (a << 4);
@ -56,25 +56,25 @@ inline unsigned hash_ull(unsigned long long a) {
return static_cast<unsigned>(a); return static_cast<unsigned>(a);
} }
inline unsigned combine_hash(unsigned h1, unsigned h2) { static inline unsigned combine_hash(unsigned h1, unsigned h2) {
h2 -= h1; h2 ^= (h1 << 8); h2 -= h1; h2 ^= (h1 << 8);
h1 -= h2; h2 ^= (h1 << 16); h1 -= h2; h2 ^= (h1 << 16);
h2 -= h1; h2 ^= (h1 << 10); h2 -= h1; h2 ^= (h1 << 10);
return h2; return h2;
} }
inline unsigned hash_u_u(unsigned a, unsigned b) { static inline unsigned hash_u_u(unsigned a, unsigned b) {
return combine_hash(hash_u(a), hash_u(b)); return combine_hash(hash_u(a), hash_u(b));
} }
unsigned string_hash(std::string_view str, unsigned init_value); unsigned string_hash(std::string_view str, unsigned init_value);
inline unsigned unsigned_ptr_hash(std::span<unsigned const> vec, unsigned init_value) { static 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); return string_hash(std::string_view(reinterpret_cast<char const*>(vec.data()), vec.size() * sizeof(unsigned)), init_value);
} }
// Backward compatibility overload // Backward compatibility overload
inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) { static inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
return unsigned_ptr_hash(std::span<unsigned const>(vec, len), init_value); return unsigned_ptr_hash(std::span<unsigned const>(vec, len), init_value);
} }
@ -251,7 +251,7 @@ struct ptr_hash {
} }
}; };
inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) { static inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) {
mix(a, b, c); mix(a, b, c);
return c; return c;
} }

8
src/util/sign.h
View file

@ -18,7 +18,7 @@ Author:
#pragma once #pragma once
typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign; typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign;
inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } }; static inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); } static inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); } static inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
inline bool is_zero(sign s) { return s == sign_zero; } static inline bool is_zero(sign s) { return s == sign_zero; }

6
src/util/tptr.h
View file

@ -44,17 +44,17 @@ Revision History:
#define UNBOXINT(PTR) static_cast<int>(reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) #define UNBOXINT(PTR) static_cast<int>(reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT)
template <typename U, typename T> template <typename U, typename T>
U unbox(T* ptr) { inline U unbox(T* ptr) {
return static_cast<U>(reinterpret_cast<std::uintptr_t>(ptr) >> PTR_ALIGNMENT); return static_cast<U>(reinterpret_cast<std::uintptr_t>(ptr) >> PTR_ALIGNMENT);
} }
template <typename T> template <typename T>
unsigned get_tag(T* ptr) { inline unsigned get_tag(T* ptr) {
return reinterpret_cast<std::uintptr_t>(ptr) & TAG_MASK; return reinterpret_cast<std::uintptr_t>(ptr) & TAG_MASK;
} }
template <typename T, typename U> template <typename T, typename U>
T* box(U val, std::uintptr_t tag = 0) { inline T* box(U val, std::uintptr_t tag = 0) {
static_assert( sizeof(T*) >= sizeof(U) + PTR_ALIGNMENT ); static_assert( sizeof(T*) >= sizeof(U) + PTR_ALIGNMENT );
SASSERT_EQ(tag & PTR_MASK, 0); SASSERT_EQ(tag & PTR_MASK, 0);
T* ptr = reinterpret_cast<T*>((static_cast<std::uintptr_t>(val) << PTR_ALIGNMENT) | tag); T* ptr = reinterpret_cast<T*>((static_cast<std::uintptr_t>(val) << PTR_ALIGNMENT) | tag);

4
src/util/util.h
View file

@ -80,14 +80,14 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
# define Z3_fallthrough # define Z3_fallthrough
#endif #endif
inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; } static inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
/** /**
\brief Return the next power of two that is greater than or equal to v. \brief Return the next power of two that is greater than or equal to v.
\warning This function returns 0 for v == 0. \warning This function returns 0 for v == 0.
*/ */
inline unsigned next_power_of_two(unsigned v) { static inline unsigned next_power_of_two(unsigned v) {
v--; v--;
v |= v >> 1; v |= v >> 1;
v |= v >> 2; v |= v >> 2;