mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Improve hash combining to avoid bitvector hash-table cliff

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-14 01:40:11 +00:00 • committed by GitHub
parent eddbc43f03
commit 0452362e9f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/chashtable.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "util/hashtable.h"
#include "util/hash.h"
#include "util/util.h"
#include <array>
#include <iostream>
typedef chashtable<int, int_hash, default_eq<int> > int_table;
@ -172,6 +173,22 @@ static void tst6() {
});
}
static void tst_combine_hash_low_bits() {
constexpr unsigned num_buckets = 1 << 12;
constexpr unsigned mask = num_buckets - 1;
std::array<bool, num_buckets> seen{};
unsigned num_seen = 0;
for (unsigned i = 0; i < (1u << 16); ++i) {
unsigned h = combine_hash(i << 12, 0x12345678u);
unsigned b = h & mask;
if (!seen[b]) {
seen[b] = true;
++num_seen;
}
}
ENSURE(num_seen > 3000);
}
void tst_chashtable() {
tst1();
tst2();
@ -180,5 +197,6 @@ void tst_chashtable() {
tst4<dint_table>(1000,10);
tst4<dint_table>(10000,10);
tst4<int_table>(50000,1000);
tst_combine_hash_low_bits();
tst5();
}

7
src/util/hash.h
View file

@ -57,10 +57,8 @@ static inline unsigned hash_ull(unsigned long long a) {
}
static inline unsigned combine_hash(unsigned h1, unsigned h2) {
h2 -= h1; h2 ^= (h1 << 8);
h1 -= h2; h2 ^= (h1 << 16);
h2 -= h1; h2 ^= (h1 << 10);
return h2;
h1 ^= h2 + 0x9e3779b9 + (h1 << 6) + (h1 >> 2);
return hash_u(h1);
}
static inline unsigned hash_u_u(unsigned a, unsigned b) {
@ -256,4 +254,3 @@ static inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) {
return c;
}