From: Tim King <taking@cs.nyu.edu>
Date: Fri, 21 Jul 2017 00:04:30 +0000 (-0700)
Subject: Moving from the gnu extensions for hash maps to the c++11 hash maps
X-Git-Tag: cvc5-1.0.0~5710
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b0659e6cd342ae40b676781b5e819d5fd2b3af7;p=cvc5.git

Moving from the gnu extensions for hash maps to the c++11 hash maps

* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
---

diff --git a/configure.ac b/configure.ac
index c0cec382f..6efae69cb 100644
--- a/configure.ac
+++ b/configure.ac
@@ -826,14 +826,14 @@ AC_SUBST([CRYPTOMINISAT_LIBS])
 
 
 # Check to see if this version/architecture of GNU C++ explicitly
-# instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
+# instantiates std::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_MSG_CHECKING([whether std::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> {}; }])],
+#include <cstdint>
+#include <functional>
+namespace std { 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++])
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 6f1de6b00..f099b017a 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -20,6 +20,7 @@
 #include <iostream>
 #include <string>
 #include <typeinfo>
+#include <unordered_map>
 #include <vector>
 
 #include "expr/expr.h"
@@ -83,7 +84,7 @@ class Mapper {
   set< Type > setTypes;
   map< Type, Type > mapTypes;
   map< pair<Type, Kind>, Expr > setoperators;
-  hash_map< Expr, Expr, ExprHashFunction > substitutions;
+  unordered_map< Expr, Expr, ExprHashFunction > substitutions;
   ostringstream sout;
   ExprManager* em;
   int depth;
diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c
index 5f0c183b7..46ca66e44 100644
--- a/examples/simple_vc_compat_c.c
+++ b/examples/simple_vc_compat_c.c
@@ -19,7 +19,8 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-/* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */
+// Use this after CVC4 is properly installed.
+// #include <cvc4/bindings/compat/c/c_interface.h>
 #include "bindings/compat/c/c_interface.h"
 
 int main() {
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 3309ce442..ffb299394 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -21,7 +21,6 @@
 #include <iosfwd>
 #include <iterator>
 #include <sstream>
-#include <string>
 
 #include "base/exception.h"
 #include "base/output.h"
@@ -33,9 +32,6 @@
 #include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "util/bitvector.h"
-#include "util/hash.h"
-#include "util/integer.h"
-#include "util/rational.h"
 #include "util/sexpr.h"
 #include "util/subrange_bound.h"
 
@@ -60,22 +56,22 @@ namespace CVC3 {
 // ExprManager-to-ExprManager import).
 static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers;
 
-static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
-static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
+static std::unordered_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
+static std::unordered_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
 
 static bool typeHasExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   return i != s_typeToExpr.end();
 }
 
 static Expr typeToExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   assert(i != s_typeToExpr.end());
   return (*i).second;
 }
 
 static Type exprToType(const Expr& e) {
-  std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
+  std::unordered_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
   assert(i != s_exprToType.end());
   return (*i).second;
 }
@@ -311,8 +307,8 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
 }
 
 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const {
-  const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
-    *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
+  const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
+    *reinterpret_cast<const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
 
   return Expr(substitute(o2n));
 }
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index be0dc3393..25e3ae32f 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -49,7 +49,10 @@
 #define _cvc3__include__formula_value_h_
 
 #include <stdlib.h>
+
 #include <map>
+#include <string>
+#include <unordered_map>
 #include <utility>
 
 #include "base/exception.h"
@@ -58,7 +61,6 @@
 #include "expr/type.h"
 #include "parser/parser.h"
 #include "smt/smt_engine.h"
-#include "util/hash.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -267,7 +269,7 @@ class CVC4_PUBLIC ExprMap : public std::map<Expr, T> {
 };/* class ExprMap<T> */
 
 template <class T>
-class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
+class CVC4_PUBLIC ExprHashMap : public std::unordered_map<Expr, T, CVC4::ExprHashFunction> {
 public:
   void insert(Expr a, Expr b);
 };/* class ExprHashMap<T> */
@@ -521,8 +523,8 @@ class CVC4_PUBLIC ValidityChecker {
 
   friend class Type; // to reach in to d_exprTypeMapRemove
 
-  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
-  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
+  typedef std::unordered_map<std::string, const CVC4::Datatype*> ConstructorMap;
+  typedef std::unordered_map<std::string, std::pair<const CVC4::Datatype*, std::string>> SelectorMap;
 
   ConstructorMap d_constructors;
   SelectorMap d_selectors;
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 575bde120..b6024b65d 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -15,7 +15,7 @@
  ** which must be saved and restored as contexts are pushed and
  ** popped.  Requires that operator= be defined for the data class,
  ** and operator== for the key class.  For key types that don't have a
- ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ ** std::hash<>, you should provide an explicit HashFcn.
  **
  ** See also:
  **  CDInsertHashMap : An "insert-once" CD hash map.
@@ -82,8 +82,9 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_H
 #define __CVC4__CONTEXT__CDHASHMAP_H
 
-#include <ext/hash_map>
+#include <functional>
 #include <iterator>
+#include <unordered_map>
 #include <vector>
 
 #include "base/cvc4_assert.h"
@@ -95,7 +96,7 @@ namespace context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDOhash_map : public ContextObj {
   friend class CDHashMap<Key, Data, HashFcn>;
 
@@ -268,7 +269,7 @@ template <class Key, class Data, class HashFcn>
 class CDHashMap : public ContextObj {
 
   typedef CDOhash_map<Key, Data, HashFcn> Element;
-  typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+  typedef std::unordered_map<Key, Element*, HashFcn> table_type;
 
   friend class CDOhash_map<Key, Data, HashFcn>;
 
diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index e099f612e..a8fbc5ee2 100644
--- a/src/context/cdhashmap_forward.h
+++ b/src/context/cdhashmap_forward.h
@@ -26,15 +26,14 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 #define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 
+#include <functional>
+
 /// \cond internals
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index ef8f661fa..db679c1f7 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -34,7 +34,8 @@
 #include "cvc4_private.h"
 
 #include <deque>
-#include <ext/hash_map>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -50,14 +51,14 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class InsertHashMap {
 private:
   typedef std::deque<Key> KeyVec;
   /** A list of the keys in the map maintained as a stack. */
   KeyVec d_keys;
 
-  typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+  typedef std::unordered_map<Key, Data, HashFcn> HashMap;
   /** The hash_map used for element lookup. */
   HashMap d_hashMap;
 
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 0d265271d..e64c51c65 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -44,8 +44,9 @@
 
 #pragma once
 
-#include <ext/hash_map>
 #include <deque>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -58,7 +59,7 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class TrailHashMap {
 public:
   /** A pair of Key and Data that mirrors hash_map::value_type. */
@@ -92,7 +93,7 @@ private:
   KDTVec d_kdts;
 
 
-  typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+  typedef std::unordered_map<Key, size_t, HashFcn> PositionMap;
   typedef typename PositionMap::iterator PM_iterator;
   typedef typename PositionMap::const_iterator PM_const_iterator;
 
diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h
index b2beb83bc..970f2758c 100644
--- a/src/context/cdtrail_hashmap_forward.h
+++ b/src/context/cdtrail_hashmap_forward.h
@@ -25,14 +25,11 @@
 
 #pragma once
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
+#include <functional>
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDTrailHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
-
diff --git a/src/cvc4.i b/src/cvc4.i
index 5f90fdb7d..4768e2344 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -11,7 +11,7 @@ namespace std {
   class istream;
   class ostream;
   template <class T> class set {};
-  template <class K, class V, class H> class hash_map {};
+  template <class K, class V, class H> class unordered_map {};
 }
 
 %{
@@ -41,7 +41,7 @@ namespace CVC4 {}
 using namespace CVC4;
 
 #include <cassert>
-#include <ext/hash_map>
+#include <unordered_map>
 #include <iosfwd>
 #include <set>
 #include <string>
@@ -86,7 +86,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
 %template(pairStringType) std::pair< std::string, CVC4::Type >;
 %template(setOfType) std::set< CVC4::Type >;
-%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
+%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
 // This is unfortunate, but seems to be necessary; if we leave NULL
 // defined, swig will expand it to "(void*) 0", and some of swig's
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 4c60f94fd..70fecb871 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -23,6 +23,8 @@
 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
+#include <unordered_set>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
@@ -78,13 +80,13 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * splitter. Can happen when exploring assertion corresponding to a
    * term-ITE.
    */
-  hash_set<TNode,TNodeHashFunction> d_visited;
+  std::unordered_set<TNode,TNodeHashFunction> d_visited;
 
   /**
    * Set to track visited nodes in a dfs search done in computeITE
    * function
    */
-  hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+  std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
 
   /** current decision for the recursive call */
   SatLiteral d_curDecision;
@@ -177,7 +179,6 @@ private:
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
-
 }/* namespace CVC4 */
 
 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 28c618cb0..37c7b6a0b 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -23,7 +23,7 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 
-#include <ext/hash_map>
+#include <unordered_map>
 
 namespace CVC4 {
 namespace expr {
@@ -150,7 +150,7 @@ namespace attr {
  */
 template <class value_type>
 class AttrHash :
-    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+    public std::unordered_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
                                AttrHashFunction> {
 };/* class AttrHash<> */
@@ -161,12 +161,12 @@ class AttrHash :
  */
 template <>
 class AttrHash<bool> :
-    protected __gnu_cxx::hash_map<NodeValue*,
+    protected std::unordered_map<NodeValue*,
                                   uint64_t,
                                   AttrBoolHashFunction> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
+  typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 84588fef0..27057ca99 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -20,6 +20,7 @@
 #ifndef __CVC4__DATATYPE_H
 #define __CVC4__DATATYPE_H
 
+#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
@@ -788,16 +789,16 @@ public:
  */
 struct CVC4_PUBLIC DatatypeHashFunction {
   inline size_t operator()(const Datatype& dt) const {
-    return StringHashFunction()(dt.getName());
+    return std::hash<std::string>()(dt.getName());
   }
   inline size_t operator()(const Datatype* dt) const {
-    return StringHashFunction()(dt->getName());
+    return std::hash<std::string>()(dt->getName());
   }
   inline size_t operator()(const DatatypeConstructor& dtc) const {
-    return StringHashFunction()(dtc.getName());
+    return std::hash<std::string>()(dtc.getName());
   }
   inline size_t operator()(const DatatypeConstructor* dtc) const {
-    return StringHashFunction()(dtc->getName());
+    return std::hash<std::string>()(dtc->getName());
   }
 };/* struct DatatypeHashFunction */
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index cee154743..b0611ccbb 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -115,7 +115,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v
 
 class ExportPrivate {
 private:
-  typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
+  typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
   ExprManager* from;
   ExprManager* to;
   ExprManagerMapCollection& vmap;
@@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat
   return NodePairIteratorAdaptor<Iterator>(i);
 }
 
-Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const {
+Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const {
   ExprManagerScope ems(*this);
   return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
 }
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 57b4ff93a..d2ad45dee 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -29,8 +29,8 @@ ${includes}
 #include <stdint.h>
 #include <iostream>
 #include <iterator>
-
 #include <string>
+#include <unordered_map>
 
 #include "base/exception.h"
 #include "options/language.h"
@@ -433,7 +433,7 @@ public:
   /**
    * Substitute pairs of (ex,replacement) from the given map.
    */
-  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
+  Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/node.h b/src/expr/node.h
index 69bb98f95..7a8bafe38 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,13 +22,16 @@
 #ifndef __CVC4__NODE_H
 #define __CVC4__NODE_H
 
-#include <vector>
-#include <string>
-#include <iostream>
-#include <utility>
+#include <stdint.h>
+
 #include <algorithm>
 #include <functional>
-#include <stdint.h>
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
 
 #include "base/configuration.h"
 #include "base/cvc4_assert.h"
@@ -42,7 +45,6 @@
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/utility.h"
-#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -243,7 +245,7 @@ public:
    * member function with a similar signature.
    */
   Node substitute(TNode node, TNode replacement,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -252,7 +254,7 @@ public:
   template <class Iterator1, class Iterator2>
   Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
                   Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -260,7 +262,7 @@ public:
    */
   template <class Iterator>
   Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /** Default constructor, makes a null expression. */
   NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
@@ -943,8 +945,6 @@ inline std::ostream& operator<<(std::ostream& out,
 
 }/* CVC4 namespace */
 
-#include <ext/hash_map>
-
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
 #include "expr/type_checker.h"
@@ -1296,14 +1296,14 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
   if (node == *this) {
     return replacement;
   }
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(node, replacement, cache);
 }
 
 template <bool ref_count>
 Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   Assert(node != *this);
 
   if (getNumChildren() == 0) {
@@ -1311,7 +1311,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   }
 
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1351,7 +1351,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                     Iterator1 nodesEnd,
                                     Iterator2 replacementsBegin,
                                     Iterator2 replacementsEnd) const {
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(nodesBegin, nodesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
@@ -1363,9 +1363,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                     Iterator1 nodesEnd,
                                     Iterator2 replacementsBegin,
                                     Iterator2 replacementsEnd,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1410,7 +1410,7 @@ template <class Iterator>
 inline Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
                                     Iterator substitutionsEnd) const {
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(substitutionsBegin, substitutionsEnd, cache);
 }
 
@@ -1419,9 +1419,9 @@ template <class Iterator>
 Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
                                     Iterator substitutionsEnd,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1468,7 +1468,7 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
 
 template<bool ref_count>
 bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const {
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   if (!strict && *this == t) {
     return true;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f7a1d98d6..e440261cb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -18,7 +18,6 @@
 #include "expr/node_manager.h"
 
 #include <algorithm>
-#include <ext/hash_set>
 #include <stack>
 #include <utility>
 
@@ -36,7 +35,6 @@
 
 using namespace std;
 using namespace CVC4::expr;
-using __gnu_cxx::hash_set;
 
 namespace CVC4 {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 44c116558..f112381d8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -30,7 +30,7 @@
 
 #include <vector>
 #include <string>
-#include <ext/hash_set>
+#include <unordered_set>
 
 #include "base/tls.h"
 #include "expr/kind.h"
@@ -95,12 +95,12 @@ class NodeManager {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
   };
 
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValuePoolHashFunction,
-                              expr::NodeValuePoolEq> NodeValuePool;
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValueIDHashFunction,
-                              expr::NodeValueIDEquality> NodeValueIDSet;
+  typedef std::unordered_set<expr::NodeValue*,
+                             expr::NodeValuePoolHashFunction,
+                             expr::NodeValuePoolEq> NodeValuePool;
+  typedef std::unordered_set<expr::NodeValue*,
+                             expr::NodeValueIDHashFunction,
+                             expr::NodeValueIDEquality> NodeValueIDSet;
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
diff --git a/src/expr/record.h b/src/expr/record.h
index 685756112..7c5854db2 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__RECORD_H
 #define __CVC4__RECORD_H
 
+#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
 #include <utility>
-#include "util/hash.h"
 
 // Forward Declarations
 namespace CVC4 {
@@ -56,13 +56,13 @@ public:
 
 struct CVC4_PUBLIC RecordSelectHashFunction {
   inline size_t operator()(const RecordSelect& t) const {
-    return StringHashFunction()(t.getField());
+    return std::hash<std::string>()(t.getField());
   }
 };/* struct RecordSelectHashFunction */
 
 struct CVC4_PUBLIC RecordUpdateHashFunction {
   inline size_t operator()(const RecordUpdate& t) const {
-    return StringHashFunction()(t.getField());
+    return std::hash<std::string>()(t.getField());
   }
 };/* struct RecordUpdateHashFunction */
 
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 864ade423..7fd938a9b 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -36,8 +36,8 @@ namespace CVC4 {
 
 SymbolTable::SymbolTable() :
   d_context(new Context()),
-  d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
-  d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+  d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)),
+  d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)),
   d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
 }
 
@@ -74,7 +74,7 @@ bool SymbolTable::isBound(const std::string& name) const throw() {
 }
 
 bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
-  CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
+  CDHashMap<std::string, Expr>::iterator found =
     d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index cefa65d0a..7c3b13003 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -21,7 +21,6 @@
 
 #include <vector>
 #include <utility>
-#include <ext/hash_map>
 
 #include "expr/expr.h"
 #include "util/hash.h"
@@ -50,10 +49,11 @@ class CVC4_PUBLIC SymbolTable {
   context::Context* d_context;
 
   /** A map for expressions. */
-  context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
+  context::CDHashMap<std::string, Expr>* d_exprMap;
 
   /** A map for types. */
-  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >*
+      d_typeMap;
 
   /** A set of defined functions. */
   context::CDHashSet<Expr, ExprHashFunction> *d_functions;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 383a31dd0..a4ab2f3b7 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -31,9 +31,9 @@ TypeNode TypeNode::s_null( &expr::NodeValue::null() );
 
 TypeNode TypeNode::substitute(const TypeNode& type,
                               const TypeNode& replacement,
-                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
   // in cache?
-  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 8dd80bc37..65b422a53 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -22,11 +22,13 @@
 #ifndef __CVC4__TYPE_NODE_H
 #define __CVC4__TYPE_NODE_H
 
-#include <vector>
-#include <string>
-#include <iostream>
 #include <stdint.h>
 
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
@@ -93,7 +95,7 @@ private:
    * member function with a similar signature.
    */
   TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
-                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -102,7 +104,7 @@ private:
   template <class Iterator1, class Iterator2>
   TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
                       Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
 
 public:
 
@@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction;
 
 }/* CVC4 namespace */
 
-#include <ext/hash_map>
-
 #include "expr/node_manager.h"
 
 namespace CVC4 {
@@ -687,7 +687,7 @@ inline TypeNode TypeNode::fromType(const Type& t) {
 inline TypeNode
 TypeNode::substitute(const TypeNode& type,
                      const TypeNode& replacement) const {
-  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
   return substitute(type, replacement, cache);
 }
 
@@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin,
                      Iterator1 typesEnd,
                      Iterator2 replacementsBegin,
                      Iterator2 replacementsEnd) const {
-  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
   return substitute(typesBegin, typesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
@@ -707,9 +707,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
                               Iterator1 typesEnd,
                               Iterator2 replacementsBegin,
                               Iterator2 replacementsEnd,
-                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
   // in cache?
-  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
index 739a8d425..94d9c2f67 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -20,8 +20,9 @@
 #ifndef __CVC4__VARIABLE_TYPE_MAP_H
 #define __CVC4__VARIABLE_TYPE_MAP_H
 
+#include <unordered_map>
+
 #include "expr/expr.h"
-#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -35,13 +36,13 @@ class CVC4_PUBLIC VariableTypeMap {
    * A map Expr -> Expr, intended to be used for a mapping of variables
    * between two ExprManagers.
    */
-  std::hash_map<Expr, Expr, ExprHashFunction> d_variables;
+  std::unordered_map<Expr, Expr, ExprHashFunction> d_variables;
 
   /**
    * A map Type -> Type, intended to be used for a mapping of types
    * between two ExprManagers.
    */
-  std::hash_map<Type, Type, TypeHashFunction> d_types;
+  std::unordered_map<Type, Type, TypeHashFunction> d_types;
 
 public:
   Expr& operator[](Expr e) { return d_variables[e]; }
@@ -49,7 +50,7 @@ public:
 
 };/* class VariableTypeMap */
 
-typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap;
+typedef std::unordered_map<uint64_t, uint64_t> VarMap;
 
 struct CVC4_PUBLIC ExprManagerMapCollection {
   VariableTypeMap d_typeMap;
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 02f0566a7..c4e670f6d 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -12,21 +12,17 @@
  ** Definitions of SMT-LIB (v1) constants.
  **/
 
-#include <ext/hash_map>
-namespace std {
-  using namespace __gnu_cxx;
-}
+#include "parser/smt1/smt1.h"
 
 #include "expr/type.h"
 #include "smt/command.h"
 #include "parser/parser.h"
-#include "parser/smt1/smt1.h"
 
 namespace CVC4 {
 namespace parser {
 
-std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
-  std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap;
+std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
+  std::unordered_map<std::string, Smt1::Logic> logicMap;
   logicMap["AUFLIA"] = AUFLIA;
   logicMap["AUFLIRA"] = AUFLIRA;
   logicMap["AUFNIRA"] = AUFNIRA;
@@ -68,7 +64,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
 }
 
 Smt1::Logic Smt1::toLogic(const std::string& name) {
-  static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
+  static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap();
   return logicMap[name];
 }
 
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index 7036aad64..e9dbea1a9 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -17,10 +17,9 @@
 #ifndef __CVC4__PARSER__SMT1_H
 #define __CVC4__PARSER__SMT1_H
 
-#include <ext/hash_map>
-namespace std { using namespace __gnu_cxx; }
+#include <string>
+#include <unordered_map>
 
-#include "util/hash.h"
 #include "parser/parser.h"
 
 namespace CVC4 {
@@ -117,7 +116,7 @@ public:
 private:
 
   void addArithmeticOperators();
-  static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
+  static std::unordered_map<std::string, Logic> newLogicMap();
 };/* class Smt1 */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a2c859055..c7156635d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -117,6 +117,7 @@ namespace CVC4 {
 #include <set>
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <vector>
 
 #include "base/output.h"
@@ -150,7 +151,7 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
-static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
+static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) {
   if(closedCache.find(e) != closedCache.end()) {
     return true;
   }
@@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, Ex
 }
 
 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
-  std::hash_set<Expr, ExprHashFunction> cache;
+  std::unordered_set<Expr, ExprHashFunction> cache;
   return isClosed(e, free, cache);
 }  
   
@@ -1798,7 +1799,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Expr attexpr;
   std::vector<Expr> patexprs;
   std::vector<Expr> patconds;
-  std::hash_set<std::string, StringHashFunction> names;
+  std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
   Type type;
   std::string s;
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 3eed0e871..e470c8111 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -22,6 +22,7 @@
 #include <sstream>
 #include <stack>
 #include <string>
+#include <unordered_map>
 #include <utility>
 
 #include "parser/parser.h"
@@ -58,7 +59,7 @@ public:
 private:
   bool d_logicSet;
   LogicInfo d_logic;
-  std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+  std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // this is a user-context stack
   std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index f137a9d92..3afd29415 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -22,7 +22,8 @@
 #define __CVC4__PARSER__TPTP_H
 
 #include <cassert>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "parser/parser.h"
 #include "smt/command.h"
@@ -45,8 +46,8 @@ class Tptp : public Parser {
   Expr d_utr_op;
   Expr d_uts_op;
   // The set of expression that already have a bridge
-  std::hash_set<Expr, ExprHashFunction> d_r_converted;
-  std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
+  std::unordered_set<Expr, ExprHashFunction> d_r_converted;
+  std::unordered_map<std::string, Expr> d_distinct_objects;
   
   std::vector< pANTLR3_INPUT_STREAM > d_in_created;
 
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
index 1f89d36f6..6cbe5f863 100644
--- a/src/printer/dagification_visitor.h
+++ b/src/printer/dagification_visitor.h
@@ -19,12 +19,13 @@
 #ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
 #define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
 
+#include <string>
+#include <unordered_map>
+#include <vector>
+
 #include "expr/node.h"
 #include "util/hash.h"
 
-#include <vector>
-#include <string>
-
 namespace CVC4 {
 
 namespace context {
@@ -65,7 +66,7 @@ class DagificationVisitor {
   /**
    * A map of subexprs to their occurrence count.
    */
-  std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
+  std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
 
   /**
    * The top-most node we are visiting.
@@ -109,7 +110,7 @@ class DagificationVisitor {
    * in independently dagifying the child.  (If it is beyond the threshold
    * and occurs in more than one parent, we'll independently dagify.)
    */
-  std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
 
   /**
    * A list of all nodes that meet the occurrence threshold and therefore
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a3868fe46..3de53f866 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__ARITH__PROOF_H
 #define __CVC4__ARITH__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
@@ -45,7 +47,7 @@ class TheoryArith;
 }
 }
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 
 class ArithProof : public TheoryProof {
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 507b65fef..9a2eef9e7 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__ARRAY__PROOF_H
 #define __CVC4__ARRAY__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
@@ -94,7 +96,7 @@ class TheoryArrays;
 } /* namespace CVC4::theory::arrays */
 } /* namespace CVC4::theory */
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 class ArrayProof : public TheoryProof {
   // TODO: whatever goes in this theory
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4c390e86f..69f9e774b 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -19,12 +19,11 @@
 #ifndef __CVC4__BITVECTOR__PROOF_H
 #define __CVC4__BITVECTOR__PROOF_H
 
-//#include <cstdint>
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iostream>
 #include <set>
 #include <sstream>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "expr/expr.h"
@@ -56,11 +55,11 @@ typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
 template <class Solver> class LFSCSatProof;
 typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
-typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
-typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
-typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
+typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
+typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
 
 class BitVectorProof : public TheoryProof {
 protected:
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 0cc0bf93e..a0d7096c0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,9 +21,9 @@
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
@@ -38,9 +38,9 @@ namespace prop {
 
 class CnfProof;
 
-typedef __gnu_cxx::hash_map<prop::SatVariable, Expr> SatVarToExpr;
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode;
-typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
+typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+typedef std::unordered_set<ClauseId> ClauseIdSet;
 
 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 2510b770a..f77a96726 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -20,7 +20,9 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iosfwd>
-#include <map>
+#include <unordered_map>
+#include <unordered_set>
+
 #include "expr/node.h"
 #include "context/cdhashset.h"
 #include "context/cdhashmap.h"
@@ -96,13 +98,11 @@ enum ProofFormat {
 
 std::string append(const std::string& str, uint64_t num);
 
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
 typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
-typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
-typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction > CDNodeToNodes;
-typedef std::hash_set<ClauseId> IdHashSet;
+typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeToNodes;
+typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
+typedef std::unordered_set<ClauseId> IdHashSet;
 
 enum ProofRule {
   RULE_GIVEN,       /* input assertion */
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 74d159bec..b114ec25f 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -16,6 +16,8 @@
 #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
 #define __CVC4__PROOF_OUTPUT_CHANNEL_H
 
+#include <unordered_set>
+
 #include "theory/output_channel.h"
 
 namespace CVC4 {
@@ -42,7 +44,7 @@ public:
 
 class MyPreRegisterVisitor {
   theory::Theory* d_theory;
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+  std::unordered_set<TNode, TNodeHashFunction> d_visited;
 public:
   typedef void return_type;
   MyPreRegisterVisitor(theory::Theory* theory);
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index d7ac80fc8..7c0660a83 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -20,14 +20,16 @@
 #pragma once
 
 #include <set>
-#include <vector>
 #include <sstream>
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 typedef std::pair<Node, Node> NodePair;
 typedef std::set<NodePair> NodePairSet;
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 7c9631896..6b2b39fd4 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -21,11 +21,10 @@
 
 #include <stdint.h>
 
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iosfwd>
 #include <set>
 #include <sstream>
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -101,18 +100,18 @@ class TSatProof {
 
   typedef std::set<typename Solver::TLit> LitSet;
   typedef std::set<typename Solver::TVar> VarSet;
-  typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap;
-  typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
+  typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
+  typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
   typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
   typedef context::CDHashMap<int, ClauseId> UnitIdMap;
   typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
-  typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap;
+  typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
   typedef std::vector<ResolutionChain*> ResStack;
   typedef std::set<ClauseId> IdSet;
   typedef std::vector<typename Solver::TLit> LitVector;
-  typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&>
+  typedef std::unordered_map<ClauseId, typename Solver::TClause&>
       IdToMinisatClause;
-  typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts;
+  typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
 
  public:
   TSatProof(Solver* solver, context::Context* context,
@@ -362,7 +361,7 @@ class TSatProof {
   IdToSatClause d_seenLemmas;
 
    private:
-  __gnu_cxx::hash_map<ClauseId, int> d_glueMap;
+  std::unordered_map<ClauseId, int> d_glueMap;
   struct Statistics {
     IntStat d_numLearnedClauses;
     IntStat d_numLearnedInProof;
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp
index 2234b7b19..a666e23d3 100644
--- a/src/proof/skolemization_manager.cpp
+++ b/src/proof/skolemization_manager.cpp
@@ -57,11 +57,11 @@ void SkolemizationManager::clear() {
   d_skolemToDisequality.clear();
 }
 
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
   return d_disequalityToSkolem.begin();
 }
 
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
   return d_disequalityToSkolem.end();
 }
 
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index 02aa6b6f0..7ec594859 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -21,7 +21,8 @@
 #define __CVC4__SKOLEMIZATION_MANAGER_H
 
 #include <iostream>
-#include <map>
+#include <unordered_map>
+
 #include "proof/proof.h"
 #include "util/proof.h"
 #include "expr/node.h"
@@ -39,12 +40,12 @@ public:
   bool isSkolem(Node skolem);
   void clear();
 
-  std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
-  std::hash_map<Node, Node, NodeHashFunction>::const_iterator end();
+  std::unordered_map<Node, Node, NodeHashFunction>::const_iterator begin();
+  std::unordered_map<Node, Node, NodeHashFunction>::const_iterator end();
 
 private:
-  std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
-  std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
+  std::unordered_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
+  std::unordered_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
 };
 
 }/* CVC4 namespace */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 541e4ce82..15ac533b7 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -20,8 +20,9 @@
 #ifndef __CVC4__THEORY_PROOF_H
 #define __CVC4__THEORY_PROOF_H
 
-#include <ext/hash_set>
 #include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "expr/expr.h"
 #include "proof/clause_id.h"
@@ -35,11 +36,11 @@ namespace theory {
 class Theory;
 } /* namespace CVC4::theory */
 
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
+typedef std::unordered_map < ClauseId, prop::SatClause* > IdToSatClause;
 
 class TheoryProof;
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef std::unordered_set<Expr, ExprHashFunction > ExprSet;
 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
 
 typedef std::set<theory::TheoryId> TheoryIdSet;
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 1fb1c4683..b817ceb69 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__UF__PROOF_H
 #define __CVC4__UF__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "theory/uf/equality_engine.h"
@@ -45,7 +47,7 @@ class TheoryUF;
 }
 }
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 
 class UFProof : public TheoryProof {
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index d626a5d15..0213ef7e3 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -990,7 +990,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               if(d_bvp){
                  ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT);
                  PSTATS(
-                 __gnu_cxx::hash_set<int> cl_levels;
+                 std::unordered_set<int> cl_levels;
                  for (int i = 0; i < learnt_clause.size(); ++i) {
                    cl_levels.insert(level(var(learnt_clause[i])));
                  }
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 555495149..485eb8535 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_Solver_h
 #define BVMinisat_Solver_h
 
-#include <ext/hash_set>
 #include <vector>
 
 #include "context/context.h"
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index affcc2999..80f8742a3 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -25,8 +25,6 @@
 #ifndef __CVC4__PROP__CNF_STREAM_H
 #define __CVC4__PROP__CNF_STREAM_H
 
-#include <ext/hash_map>
-
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 0bf5d5d7c..2b58f2f17 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 
 #include <iostream>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "options/prop_options.h"
@@ -1219,7 +1220,7 @@ lbool Solver::search(int nof_conflicts)
                 PROOF(
                       ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
                       PSTATS(
-                      __gnu_cxx::hash_set<int> cl_levels;
+                      std::unordered_set<int> cl_levels;
                       for (int i = 0; i < learnt_clause.size(); ++i) {
                         cl_levels.insert(level(var(learnt_clause[i])));
                       }
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 510a12eb2..67d3b3b7e 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -24,6 +24,7 @@
 #define __CVC4_USE_MINISAT
 
 #include <iosfwd>
+#include <unordered_set>
 
 #include "context/cdqueue.h"
 #include "expr/expr_stream.h"
@@ -138,7 +139,7 @@ public:
    * Set of all lemmas that have been "shared" in the portfolio---i.e.,
    * all imported and exported lemmas.
    */
-  std::hash_set<Node, NodeHashFunction> d_shared;
+  std::unordered_set<Node, NodeHashFunction> d_shared;
 
   /**
    * Statistic: the number of replayed decisions (via --replay).
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 837968aa2..704303826 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,7 +18,8 @@
 
 #include <algorithm>
 #include <cctype>
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <iterator>
 #include <sstream>
 #include <stack>
@@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener {
 class SmtEnginePrivate : public NodeManagerListener {
   SmtEngine& d_smt;
 
-  typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
-  typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
   /**
    * Manager for limiting time and abstract resource usage.
@@ -634,7 +635,7 @@ private:
    * conjuncts.
    */
   size_t removeFromConjunction(Node& n,
-                               const std::hash_set<unsigned long>& toRemove);
+                               const std::unordered_set<unsigned long>& toRemove);
 
   /** Scrub miplib encodings. */
   void doMiplibTrick();
@@ -2255,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){
   return d_definedFunctions->find(nf) != d_definedFunctions->end();
 }
 
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
 
   stack< triple<Node, Node, bool> > worklist;
@@ -2295,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // maybe it's in the cache
-      hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
+      unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
       if(cacheHit != cache.end()) {
         TNode ret = (*cacheHit).second;
         result.push(ret.isNull() ? n : ret);
@@ -2427,7 +2428,7 @@ struct intToBV_stack_element {
   : node(node), children_added(false) {}
 };/* struct intToBV_stack_element */
 
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 
 Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
   // Do a topological sort of the subexpressions and substitute them
@@ -3031,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
   d_nonClausalLearnedLiterals.resize(j);
 
-  hash_set<TNode, TNodeHashFunction> s;
+  unordered_set<TNode, TNodeHashFunction> s;
   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     Node assertion = d_assertions[i];
@@ -3266,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std
   }
 }
 
-size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) {
+size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
   Assert(n.getKind() == kind::AND);
   size_t removals = 0;
   for(Node::iterator j = n.begin(); j != n.end(); ++j) {
@@ -3320,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() {
   Assert(!options::incrementalSolving());
 
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
-  hash_set<unsigned long> removeAssertions;
+  unordered_set<unsigned long> removeAssertions;
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
 
-  hash_map<TNode, Node, TNodeHashFunction> intVars;
+  unordered_map<TNode, Node, TNodeHashFunction> intVars;
   for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) {
     if(d_propagator.isAssigned(*i)) {
       Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl;
@@ -3819,9 +3820,9 @@ Result SmtEngine::quickCheck() {
 }
 
 
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
+void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return;
@@ -3845,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N
 }
 
 
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
+bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return (*it).second;
@@ -3918,7 +3919,7 @@ void SmtEnginePrivate::processAssertions() {
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
     }
@@ -3937,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::nlExtPurify() ){
-    hash_map<Node, Node, NodeHashFunction> cache;
-    hash_map<Node, Node, NodeHashFunction> bcache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> bcache;
     std::vector< Node > var_eq;
     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq));
@@ -3959,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::solveRealAsInt()) {
     Chat() << "converting reals to ints..." << endl;
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     std::vector< Node > var_eq;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq));
@@ -3975,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::solveIntAsBV() > 0) {
     Chat() << "converting ints to bit-vectors..." << endl;
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, intToBV(d_assertions[i], cache));
     }
@@ -4203,7 +4204,7 @@ void SmtEnginePrivate::processAssertions() {
       // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
 
       // cache for expression traversal
-      hash_map<Node, bool, NodeHashFunction> cache;
+      unordered_map<Node, bool, NodeHashFunction> cache;
 
       // First, find all skolems that appear in the substitution map - their associated iteExpr will need
       // to be moved to the main assertion set
@@ -4656,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << ExpandDefinitionsCommand(e);
   }
-  hash_map<Node, Node, NodeHashFunction> cache;
+  unordered_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
   n = postprocess(n, TypeNode::fromType(e.getType()));
 
@@ -4701,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   TypeNode expectedType = n.getType();
 
   // Expand, then normalize
-  hash_map<Node, Node, NodeHashFunction> cache;
+  unordered_map<Node, Node, NodeHashFunction> cache;
   n = d_private->expandDefinitions(n, cache);
   // There are two ways model values for terms are computed (for historical
   // reasons).  One way is that used in check-model; the other is that
@@ -4814,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() {
     Trace("smt") << "--- getting value of " << *i << endl;
 
     // Expand, then normalize
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     Node n = d_private->expandDefinitions(*i, cache);
     n = Rewriter::rewrite(n);
 
@@ -5056,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) {
 
     // Apply any define-funs from the problem.
     {
-      hash_map<Node, Node, NodeHashFunction> cache;
+      unordered_map<Node, Node, NodeHashFunction> cache;
       n = d_private->expandDefinitions(n, cache);
     }
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 535e6fb52..854ddc61e 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdinsert_hashmap.h"
@@ -33,7 +34,7 @@ namespace theory {
   class ContainsTermITEVisitor;
 }/* CVC4::theory namespace */
 
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveTermFormulas {
   typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h
index 244420e66..dde7e1ccd 100644
--- a/src/smt_util/nary_builder.h
+++ b/src/smt_util/nary_builder.h
@@ -20,7 +20,9 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <vector>
+
 #include "expr/node.h"
 
 namespace CVC4{
@@ -47,7 +49,7 @@ private:
   Node case_assoccomm(TNode n);
   Node case_other(TNode n);
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_cache;
 };/* class RePairAssocCommutativeOperators */
 
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 47f1caf9e..e2d0d2baf 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -15,11 +15,6 @@
  ** \todo document this file
  **/
 
-
-
-
-
-
 // Pass 1: label the ite as (constant) or (+ constant variable)
 
 #include "cvc4_private.h"
@@ -27,9 +22,9 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
 #define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
 
+#include <unordered_map>
+
 #include "expr/node.h"
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include "context/cdo.h"
 #include "context/cdtrail_hashmap.h"
 
@@ -46,7 +41,7 @@ class ArithIteUtils {
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   // cache for reduce vars
   NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
 
@@ -56,7 +51,7 @@ class ArithIteUtils {
 
 
   NodeMap d_reduceGcd;
-  typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
+  typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
   NodeIntegerMap d_gcds;
 
   Integer d_one;
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 68d4d8f1a..4a9539d49 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -19,7 +19,8 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdhashset.h"
@@ -35,12 +36,12 @@ namespace theory {
 namespace arith {
 
 //Sets of Nodes
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
 
 //Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
 typedef DenseMap<Node> ArithVarToNodeMap;
 
 inline Node mkRationalNode(const Rational& q){
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 9ba4074c1..3427edbd3 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -16,8 +16,9 @@
  **/
 #include "theory/arith/constraint.h"
 
-#include <ostream>
 #include <algorithm>
+#include <ostream>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "proof/proof.h"
@@ -1333,7 +1334,7 @@ struct ConstraintCPHash {
 };
 
 void Constraint::assertionFringe(ConstraintCPVec& v){
-  hash_set<ConstraintCP, ConstraintCPHash> visited;
+  unordered_set<ConstraintCP, ConstraintCPHash> visited;
   size_t writePos = 0;
 
   if(!v.empty()){
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 662327301..25f838567 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -75,7 +75,7 @@
 #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
 #define __CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <ext/hash_map>
+#include <unordered_map>
 #include <list>
 #include <set>
 #include <vector>
@@ -145,7 +145,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
 
 typedef context::CDList<ConstraintCP> CDConstraintList;
 
-typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
+typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
 
 typedef size_t ConstraintRuleID;
 static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 77273f609..7d41666e7 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -20,7 +20,7 @@
 
 #pragma once
 
-#include <ext/hash_map>
+#include <unordered_map>
 #include <map>
 #include <set>
 #include <vector>
@@ -179,7 +179,7 @@ private:
   int d_upId;
 
 public:
-  typedef __gnu_cxx::hash_map<int, ArithVar> RowIdMap;
+  typedef std::unordered_map<int, ArithVar> RowIdMap;
 private:
   RowIdMap d_rowId2ArithVar;
 
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index d862dabbd..5b61385f3 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -304,7 +304,7 @@ bool DioSolver::queueEmpty() const{
 }
 
 Node DioSolver::columnGcdIsOne() const{
-  std::hash_map<Node, Integer, NodeHashFunction> gcdMap;
+  std::unordered_map<Node, Integer, NodeHashFunction> gcdMap;
 
   std::deque<TrailIndex>::const_iterator iter, end;
   for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 2b8b64e75..292f2b856 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -20,6 +20,7 @@
 #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
 #define __CVC4__THEORY__ARITH__DIO_SOLVER_H
 
+#include <unordered_map>
 #include <utility>
 #include <vector>
 
@@ -68,7 +69,7 @@ private:
    * We maintain a map from the variables associated with proofs to an input constraint.
    * These variables can then be used in polynomial manipulations.
    */
-  typedef std::hash_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
+  typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
   NodeToInputConstraintIndexMap d_varToInputConstraintMap;
 
   Node proofVariableToReason(const Variable& v) const{
diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h
index 471e37fa1..0b91ed074 100644
--- a/src/theory/arith/pseudoboolean_proc.h
+++ b/src/theory/arith/pseudoboolean_proc.h
@@ -19,7 +19,7 @@
 
 #pragma once
 
-#include <ext/hash_set>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -43,7 +43,7 @@ private:
   CDNode2PairMap d_pbBounds;
   SubstitutionMap d_subCache;
 
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_learningCache;
 
   context::CDO<unsigned> d_pbs;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 13fba2c77..bd983e0bf 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -53,6 +53,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/error_set.h"
@@ -199,7 +201,7 @@ protected:
     }
   };
 
-  typedef std::hash_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
+  typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
 
   static inline int determinizeSgn(int sgn){
     return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 5fb31e93f..ab5a19858 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4268,7 +4268,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
 
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
-  std::hash_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
+  std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
 
   // TODO:
   // This is not very good for user push/pop....
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index cc5fddf25..5955fb4e4 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,10 +18,9 @@
 #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 
-#include <ext/hash_set>
-#include <ext/hash_map>
 #include <iostream>
 #include <map>
+#include <unordered_map>
 
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
@@ -92,7 +91,7 @@ public:
 };/* class Info */
 
 
-typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
+typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
 
 /**
  * Class keeping track of the following information for canonical
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index 53d935813..4a08838fe 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -23,7 +23,7 @@
 
 #include <utility>
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 
@@ -33,7 +33,7 @@ namespace arrays {
 
   class StaticFactManager {
   /** Our underlying map type. */
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
 
   /**
    * Our map of Nodes to their canonical representatives.
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index bde88abab..2f5a9a14f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -551,7 +551,7 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) {
 }
 
 void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
-  std::hash_set<TNode, TNodeHashFunction> marked;
+  std::unordered_set<TNode, TNodeHashFunction> marked;
   vector<TNode> index_trail;
   vector<TNode>::iterator it, iend;
   Node equivalence_trail = reason;
@@ -1198,7 +1198,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m )
       /*
     }
     else {
-      std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
+      std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
       if (it == d_skolemCache.end()) {
         rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
         d_skolemCache[n] = rep;
@@ -1240,7 +1240,7 @@ void TheoryArrays::presolve()
 Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual)
 {
   Node skolem;
-  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
   if (it == d_skolemCache.end()) {
     NodeManager* nm = NodeManager::currentNM();
     skolem = nm->mkSkolem(name, type, comment);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7e8831733..3ef9578ef 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
+#include <unordered_map>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
@@ -384,7 +386,7 @@ class TheoryArrays : public Theory {
   // When a new read term is created, we check the index to see if we know the model value.  If so, we add it to d_constReads (and d_constReadsList)
   // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time.
   // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time.
-  typedef std::hash_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
+  typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
   CNodeNListMap d_constReads;
   context::CDList<TNode> d_reads;
   context::CDList<TNode> d_constReadsList;
@@ -408,7 +410,7 @@ class TheoryArrays : public Theory {
   };/* class ContextPopper */
   ContextPopper d_contextPopper;
 
-  std::hash_map<Node, Node, NodeHashFunction> d_skolemCache;
+  std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache;
   context::CDO<unsigned> d_skolemIndex;
   std::vector<Node> d_skolemAssertions;
 
@@ -425,7 +427,7 @@ class TheoryArrays : public Theory {
   typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap;
   DefValMap d_defValues;
 
-  typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
+  typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
   ReadBucketMap d_readBucketTable;
   context::Context* d_readTableContext;
   context::CDList<Node> d_arrayMerges;
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 4a05f3789..04d199971 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -20,6 +20,9 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/rewriter.h"
 #include "theory/type_enumerator.h"
 
@@ -150,9 +153,9 @@ public:
     // Bad case: have to recompute value counts and/or possibly switch out
     // default value
     store = n;
-    std::hash_set<TNode, TNodeHashFunction> indexSet;
-    std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap;
-    std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it;
+    std::unordered_set<TNode, TNodeHashFunction> indexSet;
+    std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap;
+    std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it;
     unsigned count;
     unsigned max = 0;
     TNode maxValue;
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index e896784ef..eb60f339b 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -23,7 +23,7 @@
 
 #include <utility>
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "context/cdo.h"
@@ -41,7 +41,7 @@ namespace arrays {
 template <class NodeType, class NodeHash>
 class UnionFind : context::ContextNotifyObj {
   /** Our underlying map type. */
-  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+  typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
 
   /**
    * Our map of Nodes to their canonical representatives.
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 03c811eee..78e01f690 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -19,8 +19,9 @@
 #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
-#include <vector>
 #include <functional>
+#include <unordered_map>
+#include <vector>
 
 #include "theory/theory.h"
 #include "context/context.h"
@@ -64,7 +65,7 @@ public:
     else return ASSIGNED_TO_TRUE;
   }
 
-  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
 
 private:
 
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index b5f7e37d4..8373f636b 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include <algorithm>
+#include <unordered_set>
+
 #include "theory/booleans/theory_bool_rewriter.h"
 
 namespace CVC4 {
@@ -41,7 +43,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
  */
 RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
 {
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   node_set visited;
   visited.insert(skipNode);
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index ed4b8aeb6..0d7e0ff2a 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -19,8 +19,8 @@
 #ifndef __CVC4__THEORY__BV__ABSTRACTION_H
 #define __CVC4__THEORY__BV__ABSTRACTION_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "expr/node.h"
 #include "theory/substitutions.h"
@@ -64,10 +64,10 @@ class AbstractionModule {
   };
 
   class ArgsTable {
-    __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
+    std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
     bool hasEntry(TNode signature) const;
   public:
-    typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
+    typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
     ArgsTable() {}
     void addEntry(TNode signature, const ArgsVec& args);
     ArgsTableEntry& getEntry(TNode signature);
@@ -122,16 +122,16 @@ class AbstractionModule {
 
   };
 
-  typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
-  typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
-  typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
-  typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
-  typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
-  typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
+  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
+  typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
+  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<unsigned, Node> IntNodeMap;
+  typedef std::unordered_map<unsigned, unsigned> IndexMap;
+  typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
+  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
 
   ArgsTable d_argsTable;
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index b6b2e2926..565c454e3 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -19,7 +19,8 @@
 #ifndef __CVC4__BITBLASTER_TEMPLATE_H
 #define __CVC4__BITBLASTER_TEMPLATE_H
 
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "bitblast_strategies_template.h"
@@ -58,8 +59,8 @@ namespace bv {
 
 class BitblastingRegistrar;
 
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 class AbstractionModule;
 
@@ -73,9 +74,9 @@ template <class T>
 class TBitblaster {
 protected:
   typedef std::vector<T> Bits;
-  typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction>  TermDefMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       TNodeSet;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>   ModelCache;
+  typedef std::unordered_map <Node, Bits, NodeHashFunction>  TermDefMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction>       TNodeSet;
+  typedef std::unordered_map<Node, Node, NodeHashFunction>   ModelCache;
 
   typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
   typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
@@ -258,7 +259,7 @@ public:
 
 
 class EagerBitblaster : public TBitblaster<Node> {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   // sat solver used for bitblasting and associated CnfStream
   prop::SatSolver*                   d_satSolver;
   BitblastingRegistrar*              d_bitblastingRegistrar;
@@ -305,8 +306,8 @@ public:
 }; /* class Registrar */
 
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
-  typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
-  typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
+  typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
+  typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
   
   static Abc_Ntk_t* abcAigNetwork;
   context::Context* d_nullContext;
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 380d06349..ec6cbad09 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -9,18 +9,21 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Eager bit-blasting solver. 
+ ** \brief Eager bit-blasting solver.
  **
  ** Eager bit-blasting solver.
  **/
 
 #include "cvc4_private.h"
+
+#pragma once
+
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node.h"
 #include "theory/theory_model.h"
 #include "theory/bv/theory_bv.h"
-#include <vector>
-#pragma once
-
 
 namespace CVC4 {
 namespace theory {
@@ -33,7 +36,7 @@ class AigBitblaster;
  * BitblastSolver
  */
 class EagerBitblastSolver {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet;
   AssertionSet d_assertionSet;
   /** Bitblasters */
   EagerBitblaster* d_bitblaster;
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index f85d8a835..30270b3c3 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -19,23 +19,25 @@
 #ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 #define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
-#include "context/context.h"
+#include <list>
+#include <queue>
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdqueue.h"
-#include "theory/uf/equality_engine.h"
+#include "context/context.h"
 #include "theory/theory.h"
-#include <queue>
-#include <list>
+#include "theory/uf/equality_engine.h"
+
 namespace CVC4 {
 namespace theory {
-
-
 namespace bv {
 
-typedef unsigned TermId; 
+typedef unsigned TermId;
 typedef unsigned ReasonId;
 extern const TermId UndefinedTermId;
 extern const ReasonId UndefinedReasonId;
-extern const ReasonId AxiomReasonId; 
+extern const ReasonId AxiomReasonId;
 
 class InequalityGraph : public context::ContextNotifyObj{
 
@@ -100,15 +102,15 @@ class InequalityGraph : public context::ContextNotifyObj{
     }
   }; 
 
-  typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
-  typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+  typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
+  typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
 
   typedef std::vector<InequalityEdge> Edges; 
-  typedef __gnu_cxx::hash_set<TermId> TermIdSet;
+  typedef std::unordered_set<TermId> TermIdSet;
 
   typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
   std::vector<InequalityNode> d_ineqNodes;
   std::vector< Edges > d_ineqEdges;
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index dcd3f1062..c5fe63ad6 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -20,7 +20,7 @@
 #define __CVC4__BV_QUICK_CHECK_H
 
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_set>
 
 #include "context/cdo.h"
 #include "expr/node.h"
@@ -99,7 +99,7 @@ public:
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
   void collectModelInfo(theory::TheoryModel* model, bool fullModel); 
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
+  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
   vars_iterator beginVars(); 
   vars_iterator endVars(); 
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 3730ebc90..4b4103e44 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -14,12 +14,16 @@
  ** Algebraic solver.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
-#include "cvc4_private.h"
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/bv/bv_subtheory.h"
-#include "theory/substitutions.h"
 #include "theory/bv/slicer.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace theory {
@@ -60,8 +64,8 @@ class SubstitutionEx {
     {}
   };
 
-  typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
-  typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
 
   Substitutions d_substitutions;
   SubstitutionsCache d_cache;
@@ -104,9 +108,9 @@ struct WorklistElement {
 }; 
 
 
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
-typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 
 class ExtractSkolemizer {
@@ -123,7 +127,7 @@ class ExtractSkolemizer {
     ExtractList() : base(1), extracts() {}
     void addExtract(Extract& e); 
   };
-  typedef   __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+  typedef   std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
   context::Context d_emptyContext;
   VarExtractMap d_varToExtract;
   theory::SubstitutionMap* d_modelMap;
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index c9fb81195..4bbe4327e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -18,6 +18,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_subtheory.h"
 
@@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver {
   context::CDQueue<TNode> d_bitblastQueue;
   Statistics d_statistics;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_modelCache;
   context::CDO<bool> d_validModelCache;
 
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 662f8835e..b416e019d 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -14,12 +14,16 @@
  ** Algebraic solver.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
-#include "cvc4_private.h"
-#include "theory/bv/bv_subtheory.h"
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -31,9 +35,9 @@ class Base;
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
-  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
-  typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
+  typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 
   struct Statistics {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 37d3723ac..1123d15ae 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -19,10 +19,12 @@
 #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 
-#include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_inequality_graph.h"
+#include <unordered_set>
+
 #include "context/cdhashset.h"
 #include "expr/attribute.h"
+#include "theory/bv/bv_inequality_graph.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -47,7 +49,7 @@ class InequalitySolver: public SubtheorySolver {
   InequalityGraph d_inequalityGraph;
   context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index a934cf045..93a83626e 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
 
+#include <unordered_map>
+
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
@@ -26,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
 
 class BvToBoolPreprocessor {
 
diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h
index 935cbb7ed..e335c1339 100644
--- a/src/theory/bv/bvintropow2.h
+++ b/src/theory/bv/bvintropow2.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
 #define __CVC4__THEORY__BV__BV_INTRO_POW_H
@@ -36,7 +36,7 @@ public:
   static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess);
 
 private:
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache);
 }; 
 
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index b594d5fec..dc8d333c4 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -20,7 +20,7 @@
 
 #include <vector>
 #include <list>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -79,7 +79,7 @@ public:
  * UnionFind
  * 
  */
-typedef __gnu_cxx::hash_set<TermId> TermSet;
+typedef std::unordered_set<TermId> TermSet;
 typedef std::vector<TermId> Decomposition; 
 
 struct ExtractTerm {
@@ -226,9 +226,9 @@ public:
 };
 
 class Slicer {
-  __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
-  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+  std::unordered_map<TermId, TNode> d_idToNode;
+  std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+  std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
   UnionFind d_unionFind;
   ExtractTerm registerTerm(TNode node); 
 public:
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index f8d3e6509..c20df35d5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -19,6 +19,9 @@
 #ifndef __CVC4__THEORY__BV__THEORY_BV_H
 #define __CVC4__THEORY__BV__THEORY_BV_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
@@ -51,7 +54,7 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
   std::vector<SubtheorySolver*> d_subtheories;
-  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
 
@@ -129,22 +132,22 @@ private:
    */
   Node getBVDivByZero(Kind k, unsigned width);
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   void collectFunctionSymbols(TNode term, TNodeSet& seen);
   void storeFunction(TNode func, TNode term);
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
 
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
-  __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
-  __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
+  std::unordered_map<unsigned, Node> d_BVDivByZero;
+  std::unordered_map<unsigned, Node> d_BVRemByZero;
 
 
-  typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction>  FunctionToArgs;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>  NodeToNode;
+  typedef std::unordered_map<Node, NodeSet, NodeHashFunction>  FunctionToArgs;
+  typedef std::unordered_map<Node, Node, NodeHashFunction>  NodeToNode;
   // for ackermanization
   FunctionToArgs d_funcToArgs;
   CVC4::theory::SubstitutionMap d_funcToSkolem;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 46297cb68..61f072643 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -19,6 +19,9 @@
 
 #pragma once
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -922,7 +925,7 @@ struct Count {
   {}
 };
 
-inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
   if(map.find(node) == map.end()) {
     Count c = neg? Count(0,1) : Count(1, 0);
     map[node] = c; 
@@ -945,7 +948,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant = utils::mkBitVectorOnes(size); 
   
@@ -974,7 +977,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
     children.push_back(utils::mkConst(constant)); 
   }
   
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it) {
     if (it->second.pos > 0 && it->second.neg > 0) {
@@ -1018,7 +1021,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
   std::vector<Node> processingStack;
   processingStack.push_back(node);
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+  std::unordered_set<TNode, TNodeHashFunction> processed;
   std::vector<Node> children;
   Kind kind = node.getKind(); 
   
@@ -1053,7 +1056,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant(size, (unsigned)0); 
   
@@ -1082,7 +1085,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) {
     children.push_back(utils::mkConst(constant)); 
   }
   
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it) {
     if (it->second.pos > 0 && it->second.neg > 0) {
@@ -1116,7 +1119,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
 
 
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant; 
   bool const_set = false; 
@@ -1144,7 +1147,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
 
   std::vector<Node> children;
 
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
   unsigned true_count = 0;
   bool seen_false = false; 
   for (; it != subterms.end(); ++it) {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5bae1af4f..8b8d5e003 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -17,19 +17,22 @@
 
 #include "cvc4_private.h"
 
-#pragma once 
+#pragma once
 
 #include <set>
-#include <vector>
 #include <sstream>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 namespace utils {
 
@@ -505,11 +508,11 @@ inline T gcd(T a, T b) {
   return a;
 }
 
-typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
 
 bool isCoreTerm(TNode term, TNodeBoolMap& cache);
 bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 uint64_t numNodes(TNode node, NodeSet& seen);
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index fd79e3fdc..a0333ed8b 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -19,7 +19,6 @@
 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index e32fa1e71..6d81dbab0 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -1092,7 +1092,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
     return true;
   }
 
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = d_leavesConstCache.find(e);
   if (it != d_leavesConstCache.end()) {
     return (*it).second;
@@ -1173,7 +1173,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
 
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+  std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
   it = d_simpVars.find(t);
   if (it != d_simpVars.end()) {
     return (*it).second;
@@ -1231,7 +1231,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
   d_simpContextCache[c] = result;
   return result;
 }
-typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
   if(visited.find(x) != visited.end()){
     return;
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 29f4f7f1f..4aad9a3f0 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -22,8 +22,7 @@
 #ifndef __CVC4__ITE_UTILITIES_H
 #define __CVC4__ITE_UTILITIES_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
 #include <vector>
 
 #include "expr/node.h"
@@ -80,7 +79,7 @@ public:
   size_t cache_size() const { return d_cache.size(); }
 
 private:
-  typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
   NodeBoolMap d_cache;
 };
 
@@ -100,7 +99,7 @@ public:
   }
   void clear();
 private:
-  typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_reachCount;
 
   bool d_skipVariables;
@@ -131,7 +130,7 @@ public:
   size_t cache_size() const;
 
 private:
-  typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_termITEHeight;
 }; /* class TermITEHeightCounter */
 
@@ -158,7 +157,7 @@ private:
   std::vector<Node>* d_assertions;
   IncomingArcCounter d_incoming;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_compressed;
 
   void reset();
@@ -206,7 +205,7 @@ private:
   //     constant
   // or  termITE(cnd, ConstantIte, ConstantIte)
   typedef std::vector<Node> NodeVec;
-  typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
+  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
   ConstantLeavesMap d_constantLeaves;
 
   // d_constantLeaves satisfies the following invariants:
@@ -249,23 +248,23 @@ private:
       return hash;
     }
   };/* struct ITESimplifier::NodePairHashFunction */
-  typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
+  typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
   NodePairMap d_constantIteEqualsConstantCache;
   NodePairMap d_replaceOverCache;
   NodePairMap d_replaceOverTermIteCache;
   Node replaceOver(Node n, Node replaceWith, Node simpVar);
   Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
 
-  std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
+  std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
   bool leavesAreConst(TNode e, theory::TheoryId tid);
   bool leavesAreConst(TNode e);
 
   NodePairMap d_simpConstCache;
   Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+  std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
   Node getSimpVar(TypeNode t);
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_simpContextCache;
   Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
 
@@ -314,7 +313,7 @@ private:
   Node d_true;
   Node d_false;
 
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   class CareSetPtr;
   class CareSetPtrVal {
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 4c1c93c17..5b714c2d3 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -17,7 +17,6 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
 #define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8d41c75d8..8597755c9 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -17,13 +17,10 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
-#include "util/hash.h"
-#include "context/cdo.h"
-
-#include <ext/hash_set>
 #include <map>
 
 #include "context/cdlist.h"
+#include "context/cdo.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 40a5b5849..f46b73b1c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -17,13 +17,12 @@
 #ifndef __CVC4__THEORY__QUANT_UTIL_H
 #define __CVC4__THEORY__QUANT_UTIL_H
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 93390facb..ec5fc633d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -720,7 +720,7 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
-  for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
+  for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
     Node n = *it;
     if( !ee->hasTerm( n ) ){
       ee->addTerm( n );
@@ -2288,4 +2288,3 @@ Node TermDb::getQAttrQuantIdNumNode( Node q ) {
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f187e5989..4650cc5d4 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -17,12 +17,14 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
+#include <map>
+#include <unordered_set>
+
 #include "expr/attribute.h"
 #include "theory/theory.h"
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/quant_util.h"
 
-#include <map>
 
 namespace CVC4 {
 namespace theory {
@@ -194,9 +196,9 @@ private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
-  std::hash_set< Node, NodeHashFunction > d_processed;
+  std::unordered_set< Node, NodeHashFunction > d_processed;
   /** terms processed */
-  std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
+  std::unordered_set< Node, NodeHashFunction > d_iclosure_processed;
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index d1412500e..9c621dbd6 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,25 +19,19 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
 #include "context/cdhashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
 #include "theory/theory.h"
-#include "util/hash.h"
+#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-class TheoryEngine;
-
 namespace theory {
-
 namespace quantifiers {
 
-class ModelEngine;
-class InstantiationEngine;
-
 class TheoryQuantifiers : public Theory {
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index faf14e0c7..fa1394f39 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1882,7 +1882,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         r_best = r;
       }
       //now, make sure that no other member of the class is an instance
-      std::hash_map<TNode, Node, TNodeHashFunction> cache;
+      std::unordered_map<TNode, Node, TNodeHashFunction> cache;
       r_best = getInstance( r_best, eqc, cache );
       //store that this representative was chosen at this point
       if( d_rep_score.find( r_best )==d_rep_score.end() ){
@@ -2001,7 +2001,7 @@ TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNo
 
 //helper functions
 
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
   if(cache.find(n) != cache.end()) {
     return cache[n];
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 92dfcdae5..7d8f5354b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -17,9 +17,9 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
+#include <unordered_map>
 
 #include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
@@ -449,7 +449,7 @@ private:
   /** processInferences : will merge equivalence classes in master equality engine, if possible */
   bool processInferences( Theory::Effort e );
   /** node contains */
-  Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
+  Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
   /** flatten representatives */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 27ab7615c..0c20c48a4 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
+static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {
@@ -94,7 +94,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
   if(s_rewriteStack == NULL) {
-    s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
+    s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>();
   }
 #endif
 
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 34c17a34c..beb5e946c 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -27,9 +27,9 @@ namespace sets {
 
 typedef std::map< Node, std::vector< Node > >::iterator                                         MEM_IT;
 typedef std::map< kind::Kind_t, std::vector< Node > >::iterator                                 KIND_TERM_IT;
-typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator                     TC_GRAPH_IT;
+typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator                     TC_GRAPH_IT;
 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator               TERM_IT;
-typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator   TC_IT;
+typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
 
   void TheorySetsRels::check(Theory::Effort level) {
     Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl;
@@ -240,7 +240,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
 
     Node join_image_rel = join_image_term[0];
-    std::hash_set< Node, NodeHashFunction > hasChecked;
+    std::unordered_set< Node, NodeHashFunction > hasChecked;
     Node join_image_rel_rep = getRepresentative( join_image_rel );
     std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
     MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
@@ -480,14 +480,14 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
       if( tc_graph_it != (tc_it->second).end() ) {
         (tc_graph_it->second).insert( mem_rep_snd );
       } else {
-        std::hash_set< Node, NodeHashFunction > sets;
+        std::unordered_set< Node, NodeHashFunction > sets;
         sets.insert( mem_rep_snd );
         (tc_it->second)[mem_rep_fst] = sets;
       }
     } else {
       std::map< Node, Node > exp_map;
-      std::hash_set< Node, NodeHashFunction > sets;
-      std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map;
+      std::unordered_set< Node, NodeHashFunction > sets;
+      std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
       sets.insert( mem_rep_snd );
       element_map[mem_rep_fst] = sets;
       d_tcr_tcGraph[tc_rel] = element_map;
@@ -529,7 +529,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
     if( tc_it != d_rRep_tcGraph.end() ) {
       bool isReachable = false;
-      std::hash_set<Node, NodeHashFunction> seen;
+      std::unordered_set<Node, NodeHashFunction> seen;
       isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
                      getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
       return isReachable;
@@ -537,8 +537,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     return false;
   }
 
-  void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
-                                    std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
+  void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+                                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
     if(hasSeen.find(start) == hasSeen.end()) {
       hasSeen.insert(start);
     }
@@ -550,7 +550,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
         isReachable = true;
         return;
       } else {
-        std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
+        std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
 
         while( set_it != pair_set_it->second.end() ) {
           // need to check if *set_it has been looked already
@@ -565,7 +565,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
 
   void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
     std::map< Node, Node > rel_tc_graph_exps;
-    std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph;
+    std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
 
     Node rel_rep = getRepresentative( tc_rel[0] );
     Node tc_rel_rep = getRepresentative( tc_rel );
@@ -576,10 +576,10 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
       Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
       Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
       Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
-      std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
+      std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
 
       if( rel_tc_graph_it == rel_tc_graph.end() ) {
-        std::hash_set< Node, NodeHashFunction > snd_elements;
+        std::unordered_set< Node, NodeHashFunction > snd_elements;
         snd_elements.insert( snd_element_rep );
         rel_tc_graph[fst_element_rep] = snd_elements;
         rel_tc_graph_exps[tuple_rep] = exps[i];
@@ -596,13 +596,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
   }
 
-  void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
+  void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
     Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
     for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) {
-      for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
+      for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
            snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) {
         std::vector< Node > reasons;
-        std::hash_set<Node, NodeHashFunction> seen;
+        std::unordered_set<Node, NodeHashFunction> seen;
         Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
         Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() );
         Node exp   = rel_tc_graph_exps.find( tuple )->second;
@@ -615,8 +615,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
   }
 
-  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
-                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) {
+  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
+                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
     Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
     std::vector< Node > all_reasons( reasons );
 
@@ -646,7 +646,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     seen.insert( cur_node_rep );
     TC_GRAPH_IT  cur_set = tc_graph.find( cur_node_rep );
     if( cur_set != tc_graph.end() ) {
-      for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
+      for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
            set_it != cur_set->second.end(); set_it++ ) {
         Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
         std::vector< Node > new_reasons( reasons );
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 16770671a..eb97405dc 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -17,11 +17,13 @@
 #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_
 #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "context/cdhashset.h"
+#include <unordered_set>
+
 #include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
 #include "theory/sets/rels_utils.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -103,12 +105,12 @@ private:
   std::map< Node, Node >        d_pending_facts;
 
 
-  std::hash_set< Node, NodeHashFunction >       d_rel_nodes;
+  std::unordered_set< Node, NodeHashFunction >       d_rel_nodes;
   std::map< Node, std::vector<Node> >           d_tuple_reps;
   std::map< Node, TupleTrie >                   d_membership_trie;
 
   /** Symbolic tuple variables that has been reduced to concrete ones */
-  std::hash_set< Node, NodeHashFunction >       d_symbolic_tuples;
+  std::unordered_set< Node, NodeHashFunction >       d_symbolic_tuples;
 
   /** Mapping between relation and its member representatives */
   std::map< Node, std::vector< Node > >           d_rReps_memberReps_cache;
@@ -120,8 +122,8 @@ private:
   std::map< Node, std::map<kind::Kind_t, std::vector<Node> > >                  d_terms_cache;
 
   /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
-  std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
-  std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
+  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
+  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
   std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
   std::map< Node, std::vector< Node > > d_tc_lemmas_last;
 
@@ -154,9 +156,9 @@ private:
   void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
   void buildTCGraphForRel( Node tc_rel );
   void doTCInference();
-  void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
-  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
-                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen );
+  void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
+  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
+                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
 
   void composeMembersForRels( Node );
   void computeMembersForBinOpRel( Node );
@@ -165,8 +167,8 @@ private:
   void computeMembersForJoinImageTerm( Node );
 
   bool isTCReachable( Node mem_rep, Node tc_rel );
-  void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
-                    std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
+  void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
 
 
   void addSharedTerm( TNode n );
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 3cce08398..8c3fe67d3 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -25,7 +25,7 @@ namespace theory {
 namespace sets {
 
 typedef std::set<TNode> Elements;
-typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
+typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
 
 struct FlattenedNodeTag {};
 typedef expr::Attribute<FlattenedNodeTag, bool> flattened;
@@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
     return RewriteResponse(REWRITE_DONE, n);
   }
 
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   node_set visited;
   visited.insert(skipNode);
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 6b78a1698..5ca625751 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -17,6 +17,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/theory.h"
@@ -43,7 +45,7 @@ private:
   IntStat d_statSharedTerms;
 
   // Needs to be a map from Nodes as after a backtrack they might not exist
-  typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
+  typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
 
   /** A map from atoms to a list of shared terms */
   SharedTermsMap d_atomsToTerms;
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 5a6618175..cca39a62e 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -19,9 +19,10 @@
 #ifndef __CVC4__THEORY__SUBSTITUTIONS_H
 #define __CVC4__THEORY__SUBSTITUTIONS_H
 
+//#include <algorithm>
 #include <utility>
 #include <vector>
-#include <algorithm>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "context/context.h"
@@ -51,7 +52,7 @@ public:
 
 private:
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
 
   /** The variables, in order of addition */
   NodeMap d_substitutions;
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 39cce27f9..2a84a7995 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -20,7 +20,7 @@
 #include "context/context.h"
 #include "theory/shared_terms_database.h"
 
-#include <ext/hash_map>
+#include <unordered_map>
 
 namespace CVC4 {
 
@@ -105,7 +105,7 @@ class SharedTermsVisitor {
   /**
    * Cache from preprocessing of atoms.
    */
-  typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+  typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
   TNodeVisitedMap d_visited;
 
   /**
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index f010798cd..8509e84ab 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -220,8 +220,8 @@ void Theory::debugPrintFacts() const{
   printFacts(DebugChannel.getStream());
 }
 
-std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
-  std::hash_set<TNode, TNodeHashFunction> currentlyShared;
+std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
+  std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
   for (shared_terms_iterator i = shared_terms_begin(),
            i_end = shared_terms_end(); i != i_end; ++i) {
     currentlyShared.insert (*i);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 82607a165..73102a6e2 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__THEORY__THEORY_H
 #define __CVC4__THEORY__THEORY_H
 
-#include <ext/hash_set>
 #include <iosfwd>
 #include <map>
 #include <set>
 #include <string>
+#include <unordered_set>
 
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
@@ -760,7 +760,7 @@ public:
    * This is a utility function for constructing a copy of the currently shared terms
    * in a queriable form.  As this is
    */
-  std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+  std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 
   /**
    * This allows the theory to be queried for whether a literal, lit, is
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7369b7c1f..1023071dc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1645,7 +1645,7 @@ Node TheoryEngine::getExplanation(TNode node) {
 struct AtomsCollect {
 
   std::vector<TNode> d_atoms;
-  std::hash_set<TNode, TNodeHashFunction> d_visited;
+  std::unordered_set<TNode, TNodeHashFunction> d_visited;
 
 public:
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 82283ef7b..408bff228 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -21,6 +21,7 @@
 
 #include <deque>
 #include <set>
+#include <unordered_map>
 #include <vector>
 #include <utility>
 
@@ -189,8 +190,8 @@ class TheoryEngine {
   theory::TheoryEngineModelBuilder* d_curr_model_builder;
   bool d_aloc_curr_model_builder;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   /**
   * Cache for theory-preprocessing of assertions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index b9a08e3ac..0f92f976e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -132,7 +132,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 
 Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const
 {
-  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
+  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
   if (it != d_modelCache.end()) {
     return (*it).second;
   }
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 126de1e46..c1c57795b 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -17,6 +17,9 @@
 #ifndef __CVC4__THEORY__THEORY_MODEL_H
 #define __CVC4__THEORY__THEORY_MODEL_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "smt/model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
@@ -52,7 +55,7 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
+  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
 public: 
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
@@ -140,8 +143,8 @@ public:
  */
 class TypeSet {
 public:
-  typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
-  typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
+  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
+  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
   typedef TypeSetMap::iterator iterator;
   typedef TypeSetMap::const_iterator const_iterator;
 private:
@@ -265,9 +268,9 @@ class TheoryEngineModelBuilder : public ModelBuilder
 protected:
   /** pointer to theory engine */
   TheoryEngine* d_te;
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_normalizedCache;
-  typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   std::map< Node, Node > d_constantReps;
 
   /** process build model */
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7c8e27575..5be32ab90 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -20,8 +20,8 @@
 #pragma once
 
 #include <deque>
-#include <ext/hash_map>
 #include <queue>
+#include <unordered_map>
 #include <vector>
 
 #include "base/output.h"
@@ -234,10 +234,10 @@ private:
   std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
 
   /** Map from nodes to their ids */
-  __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+  std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
   /** Map from function applications to their ids */
-  typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
+  typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
 
   /**
    * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
@@ -611,7 +611,7 @@ private:
    */
   std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
 
-  typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
+  typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
 
   /**
    * A map from pairs of disequal terms, to the reason why we deduced they are disequal.
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index cffa367cf..8a1c30ba6 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -61,7 +61,7 @@ SymmetryBreaker::Template::Template() :
 }
 
 TNode SymmetryBreaker::Template::find(TNode n) {
-  hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
+  unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
   if(i == d_reps.end()) {
     return n;
   } else {
@@ -400,8 +400,8 @@ void SymmetryBreaker::assertFormula(TNode phi) {
         break;
       }
     }
-    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
-    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+    unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
+    for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
         i != ps.end();
         ++i) {
       Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
@@ -421,9 +421,9 @@ void SymmetryBreaker::assertFormula(TNode phi) {
   }
   if(!d_template.match(phi)) {
     // we hit a bad match, extract the partitions and reset the template
-    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
+    unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
     Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
-    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+    for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
         i != ps.end();
         ++i) {
       Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index a814c670b..64ca41df2 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -46,6 +46,7 @@
 
 #include <iostream>
 #include <list>
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdlist.h"
@@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj {
   class Template {
     Node d_template;
     NodeBuilder<> d_assertions;
-    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
-    std::hash_map<TNode, TNode, TNodeHashFunction> d_reps;
+    std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
+    std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
 
     TNode find(TNode n);
     bool matchRecursive(TNode t, TNode n);
@@ -73,7 +74,7 @@ class SymmetryBreaker : public context::ContextNotifyObj {
   public:
     Template();
     bool match(TNode n);
-    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
+    std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
     Node assertions() {
       switch(d_assertions.getNumChildren()) {
       case 0: return Node::null();
@@ -91,7 +92,7 @@ public:
   typedef TNode Term;
   typedef std::list<Term> Terms;
   typedef std::set<Term> TermEq;
-  typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs;
+  typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs;
 
 private:
 
@@ -113,7 +114,7 @@ private:
   Permutations d_permutations;
   Terms d_terms;
   Template d_template;
-  std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache;
+  std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache;
   TermEqs d_termEqs;
   TermEqs d_termEqsOnly;
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 783585f8f..6d4d96a87 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -300,7 +300,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 
   vector<TNode> workList;
   workList.push_back(n);
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+  std::unordered_set<TNode, TNodeHashFunction> processed;
 
   while(!workList.empty()) {
     n = workList.back();
diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index a32dd076e..04c32f408 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -20,8 +20,10 @@
 #ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H
 #define __CVC4__UNCONSTRAINED_SIMPLIFIER_H
 
-#include <vector>
+#include <unordered_map>
+#include <unordered_set>
 #include <utility>
+#include <vector>
 
 #include "expr/node.h"
 #include "theory/substitutions.h"
@@ -37,9 +39,9 @@ class UnconstrainedSimplifier {
   /** number of expressions eliminated due to unconstrained simplification */
   IntStat d_numUnconstrainedElim;
 
-  typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
-  typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap;
-  typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
+  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
   TNodeCountMap d_visited;
   TNodeMap d_visitedOnce;
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.cpp b/src/util/regexp.cpp
index 9915d480d..c32b42bad 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -17,6 +17,7 @@
 
 #include "util/regexp.h"
 
+#include <algorithm>
 #include <iomanip>
 #include <iostream>
 
diff --git a/src/util/regexp.h b/src/util/regexp.h
index beb0ee097..e7c8c5806 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -20,11 +20,13 @@
 #ifndef __CVC4__REGEXP_H
 #define __CVC4__REGEXP_H
 
-#include <vector>
-#include <string>
+#include <algorithm>
+#include <cassert>
+#include <functional>
 #include <set>
 #include <sstream>
-#include <cassert>
+#include <string>
+#include <vector>
 
 #include "base/exception.h"
 #include "util/hash.h"
@@ -333,7 +335,7 @@ namespace strings {
 
 struct CVC4_PUBLIC StringHashFunction {
   size_t operator()(const ::CVC4::String& s) const {
-    return __gnu_cxx::hash<const char*>()(s.toString().c_str());
+    return std::hash<std::string>()(s.toString());
   }
 };/* struct StringHashFunction */
 
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index 3094345bd..af1d9ab48 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -17,6 +17,8 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include <unordered_set>
+
 #include "expr/array_store_all.h"
 #include "expr/expr_manager.h"
 #include "expr/kind.h"
@@ -252,7 +254,7 @@ std::cout<<"here\n";
 
   void testArraysInfinite() {
     TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
-    hash_set<Node, NodeHashFunction> elts;
+    unordered_set<Node, NodeHashFunction> elts;
     for(size_t i = 0; i < 1000; ++i) {
       TS_ASSERT( ! te.isFinished() );
       Node elt = *te++;