From 8b0659e6cd342ae40b676781b5e819d5fd2b3af7 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 20 Jul 2017 17:04:30 -0700
Subject: 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.
---
 src/prop/bvminisat/core/Solver.cc | 2 +-
 src/prop/bvminisat/core/Solver.h  | 1 -
 src/prop/cnf_stream.h             | 2 --
 src/prop/minisat/core/Solver.cc   | 3 ++-
 src/prop/theory_proxy.h           | 3 ++-
 5 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'src/prop')

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).
-- 
cgit v1.2.3