From e5681ac141018e2fee4bcaf46b479e12900abecd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Nov 2022 16:07:46 -0800 Subject: [PATCH] feat: replace `mixHash` implementation We are now using part of the murmur hash like Scala. For additional information and context, see https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313114719 --- src/runtime/hash.h | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/runtime/hash.h b/src/runtime/hash.h index 091cfb3acc..ff14d0a623 100644 --- a/src/runtime/hash.h +++ b/src/runtime/hash.h @@ -21,11 +21,15 @@ inline unsigned hash(unsigned h1, unsigned h2) { return h2; } -inline uint64 hash(uint64 h1, uint64 h2) { - h2 -= h1; h2 ^= (h1 << 16); - h1 -= h2; h2 ^= (h1 << 32); - h2 -= h1; h2 ^= (h1 << 20); - return h2; +inline uint64 hash(uint64 h, uint64 k) { + uint64 m = 0xc6a4a7935bd1e995; + uint64 r = 47; + k *= m; + k ^= k >> r; + k ^= m; + h ^= k; + h *= m; + return h; } inline unsigned hash_ptr(void const * ptr) {