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.

15 files changed, 119 insertions, 90 deletions

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);