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.

10 files changed, 25 insertions, 25 deletions

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....