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.

12 files changed, 55 insertions, 45 deletions

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 {