Merge branch 'master' into cleanup-regexp

5 files changed, 11 insertions, 21 deletions

diff --git a/src/util/cache.h b/src/util/cache.h
index 6f5bac8eb..38dc0fc99 100644
--- a/src/util/cache.h
+++ b/src/util/cache.h
@@ -21,8 +21,10 @@
 #ifndef __CVC4__CACHE_H
 #define __CVC4__CACHE_H
 
-#include <utility>
 #include <functional>
+#include <unordered_map>
+#include <utility>
+#include <vector>
 
 namespace CVC4 {
 
@@ -33,7 +35,7 @@ namespace CVC4 {
  */
 template <class T, class U, class Hasher = std::hash<T> >
 class Cache {
-  typedef std::hash_map<T, U, Hasher> Map;
+  typedef std::unordered_map<T, U, Hasher> Map;
   Map d_map;
   std::vector<T> d_current;
   typename Map::iterator d_result;
diff --git a/src/util/hash.h b/src/util/hash.h
index af468e25b..b04fb8bb5 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -20,13 +20,10 @@
 #ifndef __CVC4__HASH_H
 #define __CVC4__HASH_H
 
-// in case it's not been declared as a namespace yet
-namespace __gnu_cxx {}
+#include <functional>
+#include <string>
 
-#include <ext/hash_map>
-#include <ext/hash_set>
-
-namespace __gnu_cxx {
+namespace std {
 
 #ifdef CVC4_NEED_HASH_UINT64_T
 // on some versions and architectures of GNU C++, we need a
@@ -39,18 +36,10 @@ struct hash<uint64_t> {
 };/* struct hash<uint64_t> */
 #endif /* CVC4_NEED_HASH_UINT64_T */
 
-}/* __gnu_cxx namespace */
-
-// hackish: treat hash stuff as if it were in std namespace
-namespace std { using namespace __gnu_cxx; }
+}/* std namespace */
 
 namespace CVC4 {
 
-struct StringHashFunction {
-  size_t operator()(const std::string& str) const {
-    return __gnu_cxx::hash<const char*>()(str.c_str());
-  }
-};/* struct StringHashFunction */
 
 template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
 struct PairHashFunction {
diff --git a/src/util/hash.i b/src/util/hash.i
index 470447fc3..f2f1e6652 100644
--- a/src/util/hash.i
+++ b/src/util/hash.i
@@ -2,6 +2,4 @@
 #include "util/hash.h"
 %}
 
-%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const;
-
 %include "util/hash.h"
diff --git a/src/util/proof.h b/src/util/proof.h
index af68efa97..b34e4aed9 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -21,7 +21,7 @@
 #define __CVC4__PROOF_H
 
 #include <iosfwd>
-#include <ext/hash_map>
+#include <unordered_map>
 
 namespace CVC4 {
 
@@ -29,7 +29,7 @@ class Expr;
 class ProofLetCount;
 struct ExprHashFunction;
 
-typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
+typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
 
 class CVC4_PUBLIC Proof {
 public:
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 9fb8aea60..f451a8dec 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -21,6 +21,7 @@
 #define __CVC4__REGEXP_H
 
 #include <cstddef>
+#include <functional>
 #include <ostream>
 #include <string>
 #include <vector>