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.

configure.ac

@@ -826,14 +826,14 @@ AC_SUBST([CRYPTOMINISAT_LIBS])
 
 
 # Check to see if this version/architecture of GNU C++ explicitly
-# instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
+# instantiates std::hash<uint64_t> or not.  Some do, some don't.
 # See src/util/hash.h.
-AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
+AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
 AC_LANG_PUSH([C++])
 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
-#include <stdint.h>
-#include <ext/hash_map>
-namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
+#include <cstdint>
+#include <functional>
+namespace std { template<> struct hash<uint64_t> {}; }])],
                   [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
                   [AC_MSG_RESULT([yes])])
 AC_LANG_POP([C++])

examples/sets-translate/sets_translate.cpp

@@ -20,6 +20,7 @@
 #include <iostream>
 #include <string>
 #include <typeinfo>
+#include <unordered_map>
 #include <vector>
 
 #include "expr/expr.h"
@@ -83,7 +84,7 @@ class Mapper {
   set< Type > setTypes;
   map< Type, Type > mapTypes;
   map< pair<Type, Kind>, Expr > setoperators;
-  hash_map< Expr, Expr, ExprHashFunction > substitutions;
+  unordered_map< Expr, Expr, ExprHashFunction > substitutions;
   ostringstream sout;
   ExprManager* em;
   int depth;

examples/simple_vc_compat_c.c

@@ -19,7 +19,8 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-/* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */
+// Use this after CVC4 is properly installed.
+// #include <cvc4/bindings/compat/c/c_interface.h>
 #include "bindings/compat/c/c_interface.h"
 
 int main() {

src/compat/cvc3_compat.cpp

@@ -21,7 +21,6 @@
 #include <iosfwd>
 #include <iterator>
 #include <sstream>
-#include <string>
 
 #include "base/exception.h"
 #include "base/output.h"
@@ -33,9 +32,6 @@
 #include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "util/bitvector.h"
-#include "util/hash.h"
-#include "util/integer.h"
-#include "util/rational.h"
 #include "util/sexpr.h"
 #include "util/subrange_bound.h"
 
@@ -60,22 +56,22 @@ namespace CVC3 {
 // ExprManager-to-ExprManager import).
 static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers;
 
-static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
-static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
+static std::unordered_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
+static std::unordered_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
 
 static bool typeHasExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   return i != s_typeToExpr.end();
 }
 
 static Expr typeToExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   assert(i != s_typeToExpr.end());
   return (*i).second;
 }
 
 static Type exprToType(const Expr& e) {
-  std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
+  std::unordered_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
   assert(i != s_exprToType.end());
   return (*i).second;
 }
@@ -311,8 +307,8 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
 }
 
 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const {
-  const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
-    *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
+  const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
+    *reinterpret_cast<const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
 
   return Expr(substitute(o2n));
 }

src/compat/cvc3_compat.h

@@ -49,7 +49,10 @@
 #define _cvc3__include__formula_value_h_
 
 #include <stdlib.h>
+
 #include <map>
+#include <string>
+#include <unordered_map>
 #include <utility>
 
 #include "base/exception.h"
@@ -58,7 +61,6 @@
 #include "expr/type.h"
 #include "parser/parser.h"
 #include "smt/smt_engine.h"
-#include "util/hash.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -267,7 +269,7 @@ class CVC4_PUBLIC ExprMap : public std::map<Expr, T> {
 };/* class ExprMap<T> */
 
 template <class T>
-class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
+class CVC4_PUBLIC ExprHashMap : public std::unordered_map<Expr, T, CVC4::ExprHashFunction> {
 public:
   void insert(Expr a, Expr b);
 };/* class ExprHashMap<T> */
@@ -521,8 +523,8 @@ class CVC4_PUBLIC ValidityChecker {
 
   friend class Type; // to reach in to d_exprTypeMapRemove
 
-  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
-  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
+  typedef std::unordered_map<std::string, const CVC4::Datatype*> ConstructorMap;
+  typedef std::unordered_map<std::string, std::pair<const CVC4::Datatype*, std::string>> SelectorMap;
 
   ConstructorMap d_constructors;
   SelectorMap d_selectors;

src/context/cdhashmap.h

@@ -15,7 +15,7 @@
  ** which must be saved and restored as contexts are pushed and
  ** popped.  Requires that operator= be defined for the data class,
  ** and operator== for the key class.  For key types that don't have a
- ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ ** std::hash<>, you should provide an explicit HashFcn.
  **
  ** See also:
  **  CDInsertHashMap : An "insert-once" CD hash map.
@@ -82,8 +82,9 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_H
 #define __CVC4__CONTEXT__CDHASHMAP_H
 
-#include <ext/hash_map>
+#include <functional>
 #include <iterator>
+#include <unordered_map>
 #include <vector>
 
 #include "base/cvc4_assert.h"
@@ -95,7 +96,7 @@ namespace context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDOhash_map : public ContextObj {
   friend class CDHashMap<Key, Data, HashFcn>;
 
@@ -268,7 +269,7 @@ template <class Key, class Data, class HashFcn>
 class CDHashMap : public ContextObj {
 
   typedef CDOhash_map<Key, Data, HashFcn> Element;
-  typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+  typedef std::unordered_map<Key, Element*, HashFcn> table_type;
 
   friend class CDOhash_map<Key, Data, HashFcn>;
 

src/context/cdhashmap_forward.h

@@ -26,15 +26,14 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 #define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 
+#include <functional>
+
 /// \cond internals
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */

src/context/cdinsert_hashmap.h

@@ -34,7 +34,8 @@
 #include "cvc4_private.h"
 
 #include <deque>
-#include <ext/hash_map>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -50,14 +51,14 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class InsertHashMap {
 private:
   typedef std::deque<Key> KeyVec;
   /** A list of the keys in the map maintained as a stack. */
   KeyVec d_keys;
 
-  typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+  typedef std::unordered_map<Key, Data, HashFcn> HashMap;
   /** The hash_map used for element lookup. */
   HashMap d_hashMap;
 

src/context/cdtrail_hashmap.h

@@ -44,8 +44,9 @@
 
 #pragma once
 
-#include <ext/hash_map>
 #include <deque>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -58,7 +59,7 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class TrailHashMap {
 public:
   /** A pair of Key and Data that mirrors hash_map::value_type. */
@@ -92,7 +93,7 @@ class TrailHashMap {
   KDTVec d_kdts;
 
 
-  typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+  typedef std::unordered_map<Key, size_t, HashFcn> PositionMap;
   typedef typename PositionMap::iterator PM_iterator;
   typedef typename PositionMap::const_iterator PM_const_iterator;
 

src/context/cdtrail_hashmap_forward.h

@@ -25,14 +25,11 @@
 
 #pragma once
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
+#include <functional>
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDTrailHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
-

src/cvc4.i

@@ -11,7 +11,7 @@ namespace std {
   class istream;
   class ostream;
   template <class T> class set {};
-  template <class K, class V, class H> class hash_map {};
+  template <class K, class V, class H> class unordered_map {};
 }
 
 %{
@@ -41,7 +41,7 @@ namespace CVC4 {}
 using namespace CVC4;
 
 #include <cassert>
-#include <ext/hash_map>
+#include <unordered_map>
 #include <iosfwd>
 #include <set>
 #include <string>
@@ -86,7 +86,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
 %template(pairStringType) std::pair< std::string, CVC4::Type >;
 %template(setOfType) std::set< CVC4::Type >;
-%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
+%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
 // This is unfortunate, but seems to be necessary; if we leave NULL
 // defined, swig will expand it to "(void*) 0", and some of swig's

src/decision/justification_heuristic.h

@@ -23,6 +23,8 @@
 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
+#include <unordered_set>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
@@ -78,13 +80,13 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * splitter. Can happen when exploring assertion corresponding to a
    * term-ITE.
    */
-  hash_set<TNode,TNodeHashFunction> d_visited;
+  std::unordered_set<TNode,TNodeHashFunction> d_visited;
 
   /**
    * Set to track visited nodes in a dfs search done in computeITE
    * function
    */
-  hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+  std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
 
   /** current decision for the recursive call */
   SatLiteral d_curDecision;
@@ -177,7 +179,6 @@ class JustificationHeuristic : public ITEDecisionStrategy {
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
-
 }/* namespace CVC4 */
 
 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */

src/expr/attribute_internals.h

@@ -23,7 +23,7 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 
-#include <ext/hash_map>
+#include <unordered_map>
 
 namespace CVC4 {
 namespace expr {
@@ -150,7 +150,7 @@ namespace attr {
  */
 template <class value_type>
 class AttrHash :
-    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+    public std::unordered_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
                                AttrHashFunction> {
 };/* class AttrHash<> */
@@ -161,12 +161,12 @@ class AttrHash :
  */
 template <>
 class AttrHash<bool> :
-    protected __gnu_cxx::hash_map<NodeValue*,
+    protected std::unordered_map<NodeValue*,
                                   uint64_t,
                                   AttrBoolHashFunction> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
+  typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,

src/expr/datatype.h

@@ -20,6 +20,7 @@
 #ifndef __CVC4__DATATYPE_H
 #define __CVC4__DATATYPE_H
 
+#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
@@ -788,16 +789,16 @@ class CVC4_PUBLIC Datatype {
  */
 struct CVC4_PUBLIC DatatypeHashFunction {
   inline size_t operator()(const Datatype& dt) const {
-    return StringHashFunction()(dt.getName());
+    return std::hash<std::string>()(dt.getName());
   }
   inline size_t operator()(const Datatype* dt) const {
-    return StringHashFunction()(dt->getName());
+    return std::hash<std::string>()(dt->getName());
   }
   inline size_t operator()(const DatatypeConstructor& dtc) const {
-    return StringHashFunction()(dtc.getName());
+    return std::hash<std::string>()(dtc.getName());
   }
   inline size_t operator()(const DatatypeConstructor* dtc) const {
-    return StringHashFunction()(dtc->getName());
+    return std::hash<std::string>()(dtc->getName());
   }
 };/* struct DatatypeHashFunction */