From f71fdea42e2342c7d2745beedfa583d5d0ea9fa1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Jul 2013 14:15:54 -0700
Subject: [PATCH] Add hash goodies, and name::hash()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/CMakeLists.txt |  2 +-
 src/util/hash.cpp       | 63 +++++++++++++++++++++++++++++++++++++++++
 src/util/hash.h         | 20 +++++++++++++
 src/util/name.cpp       | 19 +++++++++++++
 src/util/name.h         |  1 +
 5 files changed, 104 insertions(+), 1 deletion(-)
 create mode 100644 src/util/hash.cpp
 create mode 100644 src/util/hash.h

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 7e9f1ae6b..32d313735 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1 +1 @@
-add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp)
+add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp hash.cpp)
diff --git a/src/util/hash.cpp b/src/util/hash.cpp
new file mode 100644
index 000000000..d6fc9efbf
--- /dev/null
+++ b/src/util/hash.cpp
@@ -0,0 +1,63 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+namespace lean {
+
+void mix(unsigned & a, unsigned & b, unsigned & c) {
+    a -= b; a -= c; a ^= (c>>13);
+    b -= c; b -= a; b ^= (a<<8);
+    c -= a; c -= b; c ^= (b>>13);
+    a -= b; a -= c; a ^= (c>>12);
+    b -= c; b -= a; b ^= (a<<16);
+    c -= a; c -= b; c ^= (b>>5);
+    a -= b; a -= c; a ^= (c>>3);
+    b -= c; b -= a; b ^= (a<<10);
+    c -= a; c -= b; c ^= (b>>15);
+}
+
+// Bob Jenkin's hash function.
+// http://burtleburtle.net/bob/hash/doobs.html
+unsigned hash(char const * str, unsigned length, unsigned init_value) {
+    register unsigned a, b, c, len;
+
+    /* 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 */
+    while (len >= 12) {
+        a += reinterpret_cast<unsigned const *>(str)[0];
+        b += reinterpret_cast<unsigned const *>(str)[1];
+        c += reinterpret_cast<unsigned const *>(str)[2];
+        mix(a,b,c);
+        str += 12; len -= 12;
+    }
+
+    /*------------------------------------- handle the last 11 bytes */
+    c += length;
+    switch(len) {
+        /* all the case statements fall through */
+    case 11:  c+=((unsigned)str[10]<<24);
+    case 10:  c+=((unsigned)str[9]<<16);
+    case 9 :  c+=((unsigned)str[8]<<8);
+        /* the first byte of c is reserved for the length */
+    case 8 :  b+=((unsigned)str[7]<<24);
+    case 7 :  b+=((unsigned)str[6]<<16);
+    case 6 :  b+=((unsigned)str[5]<<8);
+    case 5 :  b+=str[4];
+    case 4 :  a+=((unsigned)str[3]<<24);
+    case 3 :  a+=((unsigned)str[2]<<16);
+    case 2 :  a+=((unsigned)str[1]<<8);
+    case 1 :  a+=str[0];
+        /* case 0: nothing left to add */
+    }
+    mix(a,b,c);
+    /*-------------------------------------------- report the result */
+    return c;
+}
+
+}
diff --git a/src/util/hash.h b/src/util/hash.h
new file mode 100644
index 000000000..0e95a2f3f
--- /dev/null
+++ b/src/util/hash.h
@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+
+unsigned hash(char const * str, unsigned length, unsigned init_value);
+
+inline unsigned hash(unsigned h1, unsigned h2) {
+    h2 -= h1; h2 ^= (h1 << 8);
+    h1 -= h2; h2 ^= (h1 << 16);
+    h2 -= h1; h2 ^= (h1 << 10);
+    return h2;
+}
+
+}
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 9b6f93c0e..2c51ca8b1 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "name.h"
 #include "debug.h"
 #include "rc.h"
+#include "hash.h"
 
 namespace lean {
 
@@ -209,6 +210,24 @@ size_t name::size(char const * sep) const {
     }
 }
 
+unsigned name::hash() const {
+    if (m_imp == nullptr)
+        return 17;
+    else {
+        unsigned h = 13;
+        imp const * i = m_imp;
+        do {
+            if (i->m_is_string)
+                h = ::lean::hash(i->m_str, strlen(i->m_str), h);
+            else
+                h = ::lean::hash(h, i->m_k);
+            i = i->m_prefix;
+        }
+        while (i != nullptr);
+        return h;
+    }
+}
+
 std::ostream & operator<<(std::ostream & out, name const & n) {
     name::imp::display(out, default_name_separator, n.m_imp);
     return out;
diff --git a/src/util/name.h b/src/util/name.h
index ba90b3ba2..4b6b42b6e 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -44,6 +44,7 @@ public:
        \brief Size of the this name (in characters) when using the given separator.
     */
     size_t size(char const * sep = default_name_separator) const;
+    unsigned hash() const;
     friend std::ostream & operator<<(std::ostream & out, name const & n);
     class sep {
         name const & m_name;