1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
hash.cpp
Abstract:
Basic hash computation support.
Author:
Leonardo de Moura (leonardo) 2006-09-11.
Revision History:
--*/
#include "util/debug.h"
#include "util/hash.h"
#include <string.h>
static unsigned read_unsigned(const char *s) {
unsigned n;
memcpy(&n, s, sizeof(unsigned));
return n;
}
// I'm using Bob Jenkin's hash function.
// http://burtleburtle.net/bob/hash/doobs.html
unsigned string_hash(std::string_view str, unsigned init_value) {
unsigned a, b, c, len;
const char * data = str.data();
unsigned length = static_cast<unsigned>(str.length());
/* Set up the internal state */
len = length;
a = b = 0x9e3779b9; /* the golden ratio; an arbitrary value */
c = init_value; /* the previous hash value */
/*---------------------------------------- handle most of the key */
SASSERT(sizeof(unsigned) == 4);
while (len >= 12) {
a += read_unsigned(data);
b += read_unsigned(data+4);
c += read_unsigned(data+8);
mix(a,b,c);
data += 12; len -= 12;
}
/*------------------------------------- handle the last 11 bytes */
c += length;
switch(len) { /* all the case statements fall through */
case 11:
c+=((unsigned)(unsigned char)data[10]<<24);
Z3_fallthrough;
case 10:
c+=((unsigned)(unsigned char)data[9]<<16);
Z3_fallthrough;
case 9 :
c+=((unsigned)(unsigned char)data[8]<<8);
Z3_fallthrough;
/* the first byte of c is reserved for the length */
case 8 :
b+=((unsigned)(unsigned char)data[7]<<24);
Z3_fallthrough;
case 7 :
b+=((unsigned)(unsigned char)data[6]<<16);
Z3_fallthrough;
case 6 :
b+=((unsigned)(unsigned char)data[5]<<8);
Z3_fallthrough;
case 5 :
b+=(unsigned char)data[4];
Z3_fallthrough;
case 4 :
a+=((unsigned)(unsigned char)data[3]<<24);
Z3_fallthrough;
case 3 :
a+=((unsigned)(unsigned char)data[2]<<16);
Z3_fallthrough;
case 2 :
a+=((unsigned)(unsigned char)data[1]<<8);
Z3_fallthrough;
case 1 :
a+=(unsigned char)data[0];
/* case 0: nothing left to add */
break;
}
mix(a,b,c);
/*-------------------------------------------- report the result */
return c;
}