1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     hash.h
7 
8 Abstract:
9 
10     Basic hash computation support.
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2006-09-11.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include<algorithm>
22 #include "util/util.h"
23 
24 #define mix(a,b,c)              \
25 {                               \
26   a -= b; a -= c; a ^= (c>>13); \
27   b -= c; b -= a; b ^= (a<<8);  \
28   c -= a; c -= b; c ^= (b>>13); \
29   a -= b; a -= c; a ^= (c>>12); \
30   b -= c; b -= a; b ^= (a<<16); \
31   c -= a; c -= b; c ^= (b>>5);  \
32   a -= b; a -= c; a ^= (c>>3);  \
33   b -= c; b -= a; b ^= (a<<10); \
34   c -= a; c -= b; c ^= (b>>15); \
35 }
36 
hash_u(unsigned a)37 inline unsigned hash_u(unsigned a) {
38    a = (a+0x7ed55d16) + (a<<12);
39    a = (a^0xc761c23c) ^ (a>>19);
40    a = (a+0x165667b1) + (a<<5);
41    a = (a+0xd3a2646c) ^ (a<<9);
42    a = (a+0xfd7046c5) + (a<<3);
43    a = (a^0xb55a4f09) ^ (a>>16);
44    return a;
45 }
46 
hash_ull(unsigned long long a)47 inline unsigned hash_ull(unsigned long long a) {
48   a  = (~a) + (a << 18);
49   a ^= (a >> 31);
50   a += (a << 2) + (a << 4);
51   a ^= (a >> 11);
52   a += (a << 6);
53   a ^= (a >> 22);
54   return static_cast<unsigned>(a);
55 }
56 
combine_hash(unsigned h1,unsigned h2)57 inline unsigned combine_hash(unsigned h1, unsigned h2) {
58     h2 -= h1; h2 ^= (h1 << 8);
59     h1 -= h2; h2 ^= (h1 << 16);
60     h2 -= h1; h2 ^= (h1 << 10);
61     return h2;
62 }
63 
hash_u_u(unsigned a,unsigned b)64 inline unsigned hash_u_u(unsigned a, unsigned b) {
65     return combine_hash(hash_u(a), hash_u(b));
66 }
67 
68 unsigned string_hash(const char * str, unsigned len, unsigned init_value);
69 
unsigned_ptr_hash(unsigned const * vec,unsigned len,unsigned init_value)70 inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
71     return string_hash((char const*)(vec), len*4, init_value);
72 }
73 
74 template<typename Composite, typename GetKindHashProc, typename GetChildHashProc>
75 unsigned get_composite_hash(Composite app, unsigned n, GetKindHashProc const & khasher = GetKindHashProc(), GetChildHashProc const & chasher = GetChildHashProc()) {
76     unsigned a, b, c;
77     unsigned kind_hash = khasher(app);
78 
79     a = b = 0x9e3779b9;
80     c = 11;
81 
82     switch (n) {
83     case 0:
84         return c;
85     case 1:
86         a += kind_hash;
87         b  = chasher(app, 0);
88         mix(a, b, c);
89         return c;
90     case 2:
91         a += kind_hash;
92         b += chasher(app, 0);
93         c += chasher(app, 1);
94         mix(a, b, c);
95         return c;
96     case 3:
97         a += chasher(app, 0);
98         b += chasher(app, 1);
99         c += chasher(app, 2);
100         mix(a, b, c);
101         a += kind_hash;
102         mix(a, b, c);
103         return c;
104     default:
105         while (n >= 3) {
106             n--;
107             a += chasher(app, n);
108             n--;
109             b += chasher(app, n);
110             n--;
111             c += chasher(app, n);
112             mix(a, b, c);
113         }
114 
115         a += kind_hash;
116         switch (n) {
117         case 2:
118             b += chasher(app, 1);
119             Z3_fallthrough;
120         case 1:
121             c += chasher(app, 0);
122         }
123         mix(a, b, c);
124         return c;
125     }
126 }
127 
128 template<typename Composite>
operatordefault_kind_hash_proc129 struct default_kind_hash_proc { unsigned operator()(Composite const & c) const { return 17; } };
130 
131 struct int_hash {
132     typedef int data;
operatorint_hash133     unsigned operator()(int x) const { return static_cast<unsigned>(x); }
134 };
135 
136 struct unsigned_hash {
137     typedef unsigned data;
operatorunsigned_hash138     unsigned operator()(unsigned x) const { return x; }
139 };
140 
141 struct size_t_hash {
142     typedef size_t data;
operatorsize_t_hash143     unsigned operator()(size_t x) const { return static_cast<unsigned>(x); }
144 };
145 
146 struct uint64_hash {
147     typedef uint64_t data;
operatoruint64_hash148     unsigned operator()(uint64_t x) const { return static_cast<unsigned>(x); }
149 };
150 
151 struct bool_hash {
152     typedef bool data;
operatorbool_hash153     unsigned operator()(bool x) const { return static_cast<unsigned>(x); }
154 };
155 
156 template<typename T>
157 struct obj_hash {
158     typedef T data;
operatorobj_hash159     unsigned operator()(const T & e) const {
160         return e.hash();
161     }
162 };
163 
164 template<typename T>
165 struct obj_ptr_hash {
166     typedef T * data;
operatorobj_ptr_hash167     unsigned operator()(T * a) const {
168         return a->hash();
169     }
170 };
171 
172 template<typename T1, typename T2>
173 struct obj_ptr_pair_hash {
174     typedef std::pair<T1*, T2*> data;
operatorobj_ptr_pair_hash175     unsigned operator()(data const & d) const {
176         return combine_hash(d.first->hash(), d.second->hash());
177     }
178 };
179 
180 template<typename T1, typename T2, typename T3>
181 struct triple {
182     T1 first;
183     T2 second;
184     T3 third;
tripletriple185     triple(): first(T1()), second(T2()), third(T3()) {}
tripletriple186     triple(T1 f, T2 s, T3 t): first(f), second(s), third(t) {}
187 
188     bool operator==(triple const& other) const {
189         return
190             first == other.first &&
191             second == other.second &&
192             third == other.third;
193     }
194 };
195 
196 template<typename Hash1, typename Hash2, typename Hash3>
197 struct triple_hash : private Hash1 {
198     Hash2 m_hash2;
199     Hash3 m_hash3;
200     typedef triple<typename Hash1::data, typename Hash2::data, typename Hash3::data> data;
201     triple_hash(Hash1 const & h1 = Hash1(), Hash2 const & h2 = Hash2(), Hash3 const & h3 = Hash3()):
Hash1triple_hash202         Hash1(h1),
203         m_hash2(h2),
204         m_hash3(h3) {
205     }
206 
operatortriple_hash207     unsigned operator()(std::pair<typename Hash1::data, typename Hash2::data> const & p) const {
208         return combine_hash(combine_hash(Hash1::operator()(p.first), m_hash2.operator()(p.second)), m_hash3.operator()(p.third));
209     }
210 };
211 
212 template<typename T1, typename T2, typename T3>
213 struct obj_ptr_triple_hash {
214     typedef triple<T1*, T2*, T3*> data;
operatorobj_ptr_triple_hash215     unsigned operator()(data const & d) const {
216         return combine_hash(combine_hash(d.first->hash(), d.second->hash()), d.third->hash());
217     }
218 };
219 
220 template<typename Hash1, typename Hash2>
221 struct pair_hash : private Hash1 {
222     Hash2 m_hash2;
223     typedef std::pair<typename Hash1::data, typename Hash2::data> data;
224     pair_hash(Hash1 const & h1 = Hash1(), Hash2 const & h2 = Hash2()):
Hash1pair_hash225         Hash1(h1),
226         m_hash2(h2) {
227     }
228 
operatorpair_hash229     unsigned operator()(std::pair<typename Hash1::data, typename Hash2::data> const & p) const {
230         return combine_hash(Hash1::operator()(p.first), m_hash2.operator()(p.second));
231     }
232 };
233 
234 template<typename T>
get_ptr_hash(T * ptr)235 inline unsigned get_ptr_hash(T * ptr) {
236     return static_cast<unsigned>(reinterpret_cast<size_t>(ptr));
237 }
238 
239 template<typename T>
240 struct ptr_hash {
241     typedef T * data;
operatorptr_hash242     unsigned operator()(T * ptr) const {
243         return get_ptr_hash(ptr);
244     }
245 };
246 
mk_mix(unsigned a,unsigned b,unsigned c)247 inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) {
248     mix(a, b, c);
249     return c;
250 }
251 
252 
253