fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on platforms that need it; fixes Mac builds.

3 files changed, 21 insertions, 7 deletions

diff --git a/configure.ac b/configure.ac
index 6f5568bd2..4b079facf 100644
--- a/configure.ac
+++ b/configure.ac
@@ -676,6 +676,19 @@ if test "$enable_profiling" = yes; then
   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
 fi
 
+# Check to see if this version/architecture of GNU C++ explicitly
+# instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
+# See src/util/hash.h.
+AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
+AC_LANG_PUSH([C++])
+AC_COMPILE_IFELSE(AC_LANG_SOURCE([
+#include <stdint.h>
+#include <ext/hash_map>
+namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }]),
+                  [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
+                  [AC_MSG_RESULT([yes])])
+AC_LANG_POP([C++])
+
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
 
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index 264ae0e4b..6e79d6997 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -50,7 +50,7 @@ public:
   Pickle();
   Pickle(const Pickle& p);
   ~Pickle();
-  Pickle& operator = (const Pickle& other);
+  Pickle& operator=(const Pickle& other);
 };/* class Pickle */
 
 class CVC4_PUBLIC PicklingException : public Exception {
@@ -116,11 +116,11 @@ public:
 protected:
 
   virtual uint64_t variableToMap(uint64_t x) const
-    throw(AssertionException, PicklingException){
+    throw(AssertionException, PicklingException) {
     VarMap::const_iterator i = d_toMap.find(x);
-    if(i != d_toMap.end()){
+    if(i != d_toMap.end()) {
       return i->second;
-    }else{
+    } else {
       throw PicklingException();
     }
   }
diff --git a/src/util/hash.h b/src/util/hash.h
index 5f0189d44..fdfbf4087 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -29,15 +29,16 @@ namespace __gnu_cxx {}
 
 namespace __gnu_cxx {
 
-#if __WORDSIZE == 32
-// on 32-bit, we need a specialization of hash for 64-bit values
+#ifdef CVC4_NEED_HASH_UINT64_T
+// on some versions and architectures of GNU C++, we need a
+// specialization of hash for 64-bit values
 template <>
 struct hash<uint64_t> {
   size_t operator()(uint64_t v) const {
     return v;
   }
 };/* struct hash<uint64_t> */
-#endif /* 32-bit */
+#endif /* CVC4_NEED_HASH_UINT64_T */
 
 }/* __gnu_cxx namespace */