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.

6 files changed, 20 insertions, 16 deletions

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.