diff options
author | Tim King <taking@cs.nyu.edu> | 2017-07-20 17:04:30 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-20 17:04:30 -0700 |
commit | 8b0659e6cd342ae40b676781b5e819d5fd2b3af7 (patch) | |
tree | 5ac55f64d115b3e8865ce8f691f38da65fc82a94 | |
parent | 6d82ee2d1f84065ff4a86f688a3b671b85728f80 (diff) |
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.
120 files changed, 536 insertions, 494 deletions
diff --git a/configure.ac b/configure.ac index c0cec382f..6efae69cb 100644 --- a/configure.ac +++ b/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++]) diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 6f1de6b00..f099b017a 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/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; diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c index 5f0c183b7..46ca66e44 100644 --- a/examples/simple_vc_compat_c.c +++ b/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() { diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 3309ce442..ffb299394 100644 --- a/src/compat/cvc3_compat.cpp +++ b/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)); } diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index be0dc3393..25e3ae32f 100644 --- a/src/compat/cvc3_compat.h +++ b/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; diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 575bde120..b6024b65d 100644 --- a/src/context/cdhashmap.h +++ b/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>; diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h index e099f612e..a8fbc5ee2 100644 --- a/src/context/cdhashmap_forward.h +++ b/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 */ diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index ef8f661fa..db679c1f7 100644 --- a/src/context/cdinsert_hashmap.h +++ b/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; diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index 0d265271d..e64c51c65 100644 --- a/src/context/cdtrail_hashmap.h +++ b/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 @@ private: 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; diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h index b2beb83bc..970f2758c 100644 --- a/src/context/cdtrail_hashmap_forward.h +++ b/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 */ - diff --git a/src/cvc4.i b/src/cvc4.i index 5f90fdb7d..4768e2344 100644 --- a/src/cvc4.i +++ b/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 diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 4c60f94fd..70fecb871 100644 --- a/src/decision/justification_heuristic.h +++ b/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 @@ private: };/* class JustificationHeuristic */ }/* namespace decision */ - }/* namespace CVC4 */ #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 28c618cb0..37c7b6a0b 100644 --- a/src/expr/attribute_internals.h +++ b/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, diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 84588fef0..27057ca99 100644 --- a/src/expr/datatype.h +++ b/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 @@ public: */ 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 */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index cee154743..b0611ccbb 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -115,7 +115,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v class ExportPrivate { private: - typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; + typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; ExprManager* from; ExprManager* to; ExprManagerMapCollection& vmap; @@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat return NodePairIteratorAdaptor<Iterator>(i); } -Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const { +Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const { ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 57b4ff93a..d2ad45dee 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -29,8 +29,8 @@ ${includes} #include <stdint.h> #include <iostream> #include <iterator> - #include <string> +#include <unordered_map> #include "base/exception.h" #include "options/language.h" @@ -433,7 +433,7 @@ public: /** * Substitute pairs of (ex,replacement) from the given map. */ - Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const; + Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const; /** * Returns the string representation of the expression. diff --git a/src/expr/node.h b/src/expr/node.h index 69bb98f95..7a8bafe38 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -22,13 +22,16 @@ #ifndef __CVC4__NODE_H #define __CVC4__NODE_H -#include <vector> -#include <string> -#include <iostream> -#include <utility> +#include <stdint.h> + #include <algorithm> #include <functional> -#include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <unordered_set> +#include <utility> +#include <vector> #include "base/configuration.h" #include "base/cvc4_assert.h" @@ -42,7 +45,6 @@ #include "options/language.h" #include "options/set_language.h" #include "util/utility.h" -#include "util/hash.h" namespace CVC4 { @@ -243,7 +245,7 @@ public: * member function with a similar signature. */ Node substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -252,7 +254,7 @@ public: template <class Iterator1, class Iterator2> Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -260,7 +262,7 @@ public: */ template <class Iterator> Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** Default constructor, makes a null expression. */ NodeTemplate() : d_nv(&expr::NodeValue::null()) { } @@ -943,8 +945,6 @@ inline std::ostream& operator<<(std::ostream& out, }/* CVC4 namespace */ -#include <ext/hash_map> - //#include "expr/attribute.h" #include "expr/node_manager.h" #include "expr/type_checker.h" @@ -1296,14 +1296,14 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { if (node == *this) { return replacement; } - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(node, replacement, cache); } template <bool ref_count> Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { Assert(node != *this); if (getNumChildren() == 0) { @@ -1311,7 +1311,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, } // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1351,7 +1351,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } @@ -1363,9 +1363,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1410,7 +1410,7 @@ template <class Iterator> inline Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(substitutionsBegin, substitutionsEnd, cache); } @@ -1419,9 +1419,9 @@ template <class Iterator> Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1468,7 +1468,7 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { template<bool ref_count> bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; if (!strict && *this == t) { return true; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f7a1d98d6..e440261cb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -18,7 +18,6 @@ #include "expr/node_manager.h" #include <algorithm> -#include <ext/hash_set> #include <stack> #include <utility> @@ -36,7 +35,6 @@ using namespace std; using namespace CVC4::expr; -using __gnu_cxx::hash_set; namespace CVC4 { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 44c116558..f112381d8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,7 +30,7 @@ #include <vector> #include <string> -#include <ext/hash_set> +#include <unordered_set> #include "base/tls.h" #include "expr/kind.h" @@ -95,12 +95,12 @@ class NodeManager { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } }; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValuePoolHashFunction, - expr::NodeValuePoolEq> NodeValuePool; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValueIDHashFunction, - expr::NodeValueIDEquality> NodeValueIDSet; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValuePoolHashFunction, + expr::NodeValuePoolEq> NodeValuePool; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValueIDHashFunction, + expr::NodeValueIDEquality> NodeValueIDSet; static CVC4_THREADLOCAL(NodeManager*) s_current; diff --git a/src/expr/record.h b/src/expr/record.h index 685756112..7c5854db2 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -19,11 +19,11 @@ #ifndef __CVC4__RECORD_H #define __CVC4__RECORD_H +#include <functional> #include <iostream> #include <string> #include <vector> #include <utility> -#include "util/hash.h" // Forward Declarations namespace CVC4 { @@ -56,13 +56,13 @@ public: struct CVC4_PUBLIC RecordSelectHashFunction { inline size_t operator()(const RecordSelect& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordSelectHashFunction */ struct CVC4_PUBLIC RecordUpdateHashFunction { inline size_t operator()(const RecordUpdate& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordUpdateHashFunction */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 864ade423..7fd938a9b 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -36,8 +36,8 @@ namespace CVC4 { SymbolTable::SymbolTable() : d_context(new Context()), - d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)), - d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), + d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)), + d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)), d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) { } @@ -74,7 +74,7 @@ bool SymbolTable::isBound(const std::string& name) const throw() { } bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() { - CDHashMap<std::string, Expr, StringHashFunction>::iterator found = + CDHashMap<std::string, Expr>::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cefa65d0a..7c3b13003 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -21,7 +21,6 @@ #include <vector> #include <utility> -#include <ext/hash_map> #include "expr/expr.h" #include "util/hash.h" @@ -50,10 +49,11 @@ class CVC4_PUBLIC SymbolTable { context::Context* d_context; /** A map for expressions. */ - context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap; + context::CDHashMap<std::string, Expr>* d_exprMap; /** A map for types. */ - context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >* + d_typeMap; /** A set of defined functions. */ context::CDHashSet<Expr, ExprHashFunction> *d_functions; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 383a31dd0..a4ab2f3b7 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -31,9 +31,9 @@ TypeNode TypeNode::s_null( &expr::NodeValue::null() ); TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8dd80bc37..65b422a53 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -22,11 +22,13 @@ #ifndef __CVC4__TYPE_NODE_H #define __CVC4__TYPE_NODE_H -#include <vector> -#include <string> -#include <iostream> #include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <vector> + #include "base/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" @@ -93,7 +95,7 @@ private: * member function with a similar signature. */ TypeNode substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -102,7 +104,7 @@ private: template <class Iterator1, class Iterator2> TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; public: @@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; }/* CVC4 namespace */ -#include <ext/hash_map> - #include "expr/node_manager.h" namespace CVC4 { @@ -687,7 +687,7 @@ inline TypeNode TypeNode::fromType(const Type& t) { inline TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(type, replacement, cache); } @@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache); } @@ -707,9 +707,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 739a8d425..94d9c2f67 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -20,8 +20,9 @@ #ifndef __CVC4__VARIABLE_TYPE_MAP_H #define __CVC4__VARIABLE_TYPE_MAP_H +#include <unordered_map> + #include "expr/expr.h" -#include "util/hash.h" namespace CVC4 { @@ -35,13 +36,13 @@ class CVC4_PUBLIC VariableTypeMap { * A map Expr -> Expr, intended to be used for a mapping of variables * between two ExprManagers. */ - std::hash_map<Expr, Expr, ExprHashFunction> d_variables; + std::unordered_map<Expr, Expr, ExprHashFunction> d_variables; /** * A map Type -> Type, intended to be used for a mapping of types * between two ExprManagers. */ - std::hash_map<Type, Type, TypeHashFunction> d_types; + std::unordered_map<Type, Type, TypeHashFunction> d_types; public: Expr& operator[](Expr e) { return d_variables[e]; } @@ -49,7 +50,7 @@ public: };/* class VariableTypeMap */ -typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap; +typedef std::unordered_map<uint64_t, uint64_t> VarMap; struct CVC4_PUBLIC ExprManagerMapCollection { VariableTypeMap d_typeMap; diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 02f0566a7..c4e670f6d 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -12,21 +12,17 @@ ** Definitions of SMT-LIB (v1) constants. **/ -#include <ext/hash_map> -namespace std { - using namespace __gnu_cxx; -} +#include "parser/smt1/smt1.h" #include "expr/type.h" #include "smt/command.h" #include "parser/parser.h" -#include "parser/smt1/smt1.h" namespace CVC4 { namespace parser { -std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() { - std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap; +std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() { + std::unordered_map<std::string, Smt1::Logic> logicMap; logicMap["AUFLIA"] = AUFLIA; logicMap["AUFLIRA"] = AUFLIRA; logicMap["AUFNIRA"] = AUFNIRA; @@ -68,7 +64,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne } Smt1::Logic Smt1::toLogic(const std::string& name) { - static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); + static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap(); return logicMap[name]; } diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index 7036aad64..e9dbea1a9 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -17,10 +17,9 @@ #ifndef __CVC4__PARSER__SMT1_H #define __CVC4__PARSER__SMT1_H -#include <ext/hash_map> -namespace std { using namespace __gnu_cxx; } +#include <string> +#include <unordered_map> -#include "util/hash.h" #include "parser/parser.h" namespace CVC4 { @@ -117,7 +116,7 @@ public: private: void addArithmeticOperators(); - static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); + static std::unordered_map<std::string, Logic> newLogicMap(); };/* class Smt1 */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a2c859055..c7156635d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -117,6 +117,7 @@ namespace CVC4 { #include <set> #include <sstream> #include <string> +#include <unordered_set> #include <vector> #include "base/output.h" @@ -150,7 +151,7 @@ using namespace CVC4::parser; #define MK_CONST EXPR_MANAGER->mkConst #define UNSUPPORTED PARSER_STATE->unimplementedFeature -static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) { +static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) { if(closedCache.find(e) != closedCache.end()) { return true; } @@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, Ex } static inline bool isClosed(const Expr& e, std::set<Expr>& free) { - std::hash_set<Expr, ExprHashFunction> cache; + std::unordered_set<Expr, ExprHashFunction> cache; return isClosed(e, free, cache); } @@ -1798,7 +1799,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr attexpr; std::vector<Expr> patexprs; std::vector<Expr> patconds; - std::hash_set<std::string, StringHashFunction> names; + std::unordered_set<std::string> names; std::vector< std::pair<std::string, Expr> > binders; Type type; std::string s; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 3eed0e871..e470c8111 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,6 +22,7 @@ #include <sstream> #include <stack> #include <string> +#include <unordered_map> #include <utility> #include "parser/parser.h" @@ -58,7 +59,7 @@ public: private: bool d_logicSet; LogicInfo d_logic; - std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap; + std::unordered_map<std::string, Kind> operatorKindMap; std::pair<Expr, std::string> d_lastNamedTerm; // this is a user-context stack std::stack< std::map<Expr, std::string> > d_unsatCoreNames; diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index f137a9d92..3afd29415 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -22,7 +22,8 @@ #define __CVC4__PARSER__TPTP_H #include <cassert> -#include <ext/hash_set> +#include <unordered_map> +#include <unordered_set> #include "parser/parser.h" #include "smt/command.h" @@ -45,8 +46,8 @@ class Tptp : public Parser { Expr d_utr_op; Expr d_uts_op; // The set of expression that already have a bridge - std::hash_set<Expr, ExprHashFunction> d_r_converted; - std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects; + std::unordered_set<Expr, ExprHashFunction> d_r_converted; + std::unordered_map<std::string, Expr> d_distinct_objects; std::vector< pANTLR3_INPUT_STREAM > d_in_created; diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h index 1f89d36f6..6cbe5f863 100644 --- a/src/printer/dagification_visitor.h +++ b/src/printer/dagification_visitor.h @@ -19,12 +19,13 @@ #ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H #define __CVC4__PRINTER__DAGIFICATION_VISITOR_H +#include <string> +#include <unordered_map> +#include <vector> + #include "expr/node.h" #include "util/hash.h" -#include <vector> -#include <string> - namespace CVC4 { namespace context { @@ -65,7 +66,7 @@ class DagificationVisitor { /** * A map of subexprs to their occurrence count. */ - std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; + std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; /** * The top-most node we are visiting. @@ -109,7 +110,7 @@ class DagificationVisitor { * in independently dagifying the child. (If it is beyond the threshold * and occurs in more than one parent, we'll independently dagify.) */ - std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent; + std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent; /** * A list of all nodes that meet the occurrence threshold and therefore 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 { 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). diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 837968aa2..704303826 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,7 +18,8 @@ #include <algorithm> #include <cctype> -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <iterator> #include <sstream> #include <stack> @@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener { class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; - typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; - typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; + typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; + typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; /** * Manager for limiting time and abstract resource usage. @@ -634,7 +635,7 @@ private: * conjuncts. */ size_t removeFromConjunction(Node& n, - const std::hash_set<unsigned long>& toRemove); + const std::unordered_set<unsigned long>& toRemove); /** Scrub miplib encodings. */ void doMiplibTrick(); @@ -2255,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) +Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { stack< triple<Node, Node, bool> > worklist; @@ -2295,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } // maybe it's in the cache - hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n); + unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n); if(cacheHit != cache.end()) { TNode ret = (*cacheHit).second; result.push(ret.isNull() ? n : ret); @@ -2427,7 +2428,7 @@ struct intToBV_stack_element { : node(node), children_added(false) {} };/* struct intToBV_stack_element */ -typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) { // Do a topological sort of the subexpressions and substitute them @@ -3031,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; d_nonClausalLearnedLiterals.resize(j); - hash_set<TNode, TNodeHashFunction> s; + unordered_set<TNode, TNodeHashFunction> s; Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node assertion = d_assertions[i]; @@ -3266,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std } } -size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) { +size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) { Assert(n.getKind() == kind::AND); size_t removals = 0; for(Node::iterator j = n.begin(); j != n.end(); ++j) { @@ -3320,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() { Assert(!options::incrementalSolving()); const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - hash_set<unsigned long> removeAssertions; + unordered_set<unsigned long> removeAssertions; NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); - hash_map<TNode, Node, TNodeHashFunction> intVars; + unordered_map<TNode, Node, TNodeHashFunction> intVars; for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) { if(d_propagator.isAssigned(*i)) { Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl; @@ -3819,9 +3820,9 @@ Result SmtEngine::quickCheck() { } -void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache) +void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache) { - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = cache.find(n); if (it != cache.end()) { return; @@ -3845,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N } -bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache) +bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache) { - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = cache.find(n); if (it != cache.end()) { return (*it).second; @@ -3918,7 +3919,7 @@ void SmtEnginePrivate::processAssertions() { Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); } @@ -3937,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::nlExtPurify() ){ - hash_map<Node, Node, NodeHashFunction> cache; - hash_map<Node, Node, NodeHashFunction> bcache; + unordered_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> bcache; std::vector< Node > var_eq; for (unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq)); @@ -3959,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveRealAsInt()) { Chat() << "converting reals to ints..." << endl; - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; std::vector< Node > var_eq; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq)); @@ -3975,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveIntAsBV() > 0) { Chat() << "converting ints to bit-vectors..." << endl; - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, intToBV(d_assertions[i], cache)); } @@ -4203,7 +4204,7 @@ void SmtEnginePrivate::processAssertions() { // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. // cache for expression traversal - hash_map<Node, bool, NodeHashFunction> cache; + unordered_map<Node, bool, NodeHashFunction> cache; // First, find all skolems that appear in the substitution map - their associated iteExpr will need // to be moved to the main assertion set @@ -4656,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L if(Dump.isOn("benchmark")) { Dump("benchmark") << ExpandDefinitionsCommand(e); } - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); @@ -4701,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin TypeNode expectedType = n.getType(); // Expand, then normalize - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); // There are two ways model values for terms are computed (for historical // reasons). One way is that used in check-model; the other is that @@ -4814,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "--- getting value of " << *i << endl; // Expand, then normalize - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(*i, cache); n = Rewriter::rewrite(n); @@ -5056,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) { // Apply any define-funs from the problem. { - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); } Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 535e6fb52..854ddc61e 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -18,6 +18,7 @@ #pragma once +#include <unordered_map> #include <vector> #include "context/cdinsert_hashmap.h" @@ -33,7 +34,7 @@ namespace theory { class ContainsTermITEVisitor; }/* CVC4::theory namespace */ -typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; +typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap; class RemoveTermFormulas { typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache; diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h index 244420e66..dde7e1ccd 100644 --- a/src/smt_util/nary_builder.h +++ b/src/smt_util/nary_builder.h @@ -20,7 +20,9 @@ #pragma once +#include <unordered_map> #include <vector> + #include "expr/node.h" namespace CVC4{ @@ -47,7 +49,7 @@ private: Node case_assoccomm(TNode n); Node case_other(TNode n); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_cache; };/* class RePairAssocCommutativeOperators */ 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.... 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. diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 03c811eee..78e01f690 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -19,8 +19,9 @@ #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H -#include <vector> #include <functional> +#include <unordered_map> +#include <vector> #include "theory/theory.h" #include "context/context.h" @@ -64,7 +65,7 @@ public: else return ASSIGNED_TO_TRUE; } - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; private: diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index b5f7e37d4..8373f636b 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,6 +16,8 @@ **/ #include <algorithm> +#include <unordered_set> + #include "theory/booleans/theory_bool_rewriter.h" namespace CVC4 { @@ -41,7 +43,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { */ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index ed4b8aeb6..0d7e0ff2a 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -19,8 +19,8 @@ #ifndef __CVC4__THEORY__BV__ABSTRACTION_H #define __CVC4__THEORY__BV__ABSTRACTION_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> +#include <unordered_set> #include "expr/node.h" #include "theory/substitutions.h" @@ -64,10 +64,10 @@ class AbstractionModule { }; class ArgsTable { - __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; + std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; bool hasEntry(TNode signature) const; public: - typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; + typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; ArgsTable() {} void addEntry(TNode signature, const ArgsVec& args); ArgsTableEntry& getEntry(TNode signature); @@ -122,16 +122,16 @@ class AbstractionModule { }; - typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap; - typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; - typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap; - typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap; - typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<unsigned, Node> IntNodeMap; + typedef std::unordered_map<unsigned, unsigned> IndexMap; + typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap; ArgsTable d_argsTable; diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index b6b2e2926..565c454e3 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -19,7 +19,8 @@ #ifndef __CVC4__BITBLASTER_TEMPLATE_H #define __CVC4__BITBLASTER_TEMPLATE_H -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "bitblast_strategies_template.h" @@ -58,8 +59,8 @@ namespace bv { class BitblastingRegistrar; -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; class AbstractionModule; @@ -73,9 +74,9 @@ template <class T> class TBitblaster { protected: typedef std::vector<T> Bits; - typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> ModelCache; + typedef std::unordered_map <Node, Bits, NodeHashFunction> TermDefMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*); @@ -258,7 +259,7 @@ public: class EagerBitblaster : public TBitblaster<Node> { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; @@ -305,8 +306,8 @@ public: }; /* class Registrar */ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { - typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; - typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; + typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; + typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 380d06349..ec6cbad09 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -9,18 +9,21 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Eager bit-blasting solver. + ** \brief Eager bit-blasting solver. ** ** Eager bit-blasting solver. **/ #include "cvc4_private.h" + +#pragma once + +#include <unordered_set> +#include <vector> + #include "expr/node.h" #include "theory/theory_model.h" #include "theory/bv/theory_bv.h" -#include <vector> -#pragma once - namespace CVC4 { namespace theory { @@ -33,7 +36,7 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; + typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; AssertionSet d_assertionSet; /** Bitblasters */ EagerBitblaster* d_bitblaster; diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index f85d8a835..30270b3c3 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -19,23 +19,25 @@ #ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H #define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H -#include "context/context.h" +#include <list> +#include <queue> +#include <unordered_map> +#include <unordered_set> + #include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" +#include "context/context.h" #include "theory/theory.h" -#include <queue> -#include <list> +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { - - namespace bv { -typedef unsigned TermId; +typedef unsigned TermId; typedef unsigned ReasonId; extern const TermId UndefinedTermId; extern const ReasonId UndefinedReasonId; -extern const ReasonId AxiomReasonId; +extern const ReasonId AxiomReasonId; class InequalityGraph : public context::ContextNotifyObj{ @@ -100,15 +102,15 @@ class InequalityGraph : public context::ContextNotifyObj{ } }; - typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; - typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; + typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; typedef std::vector<InequalityEdge> Edges; - typedef __gnu_cxx::hash_set<TermId> TermIdSet; + typedef std::unordered_set<TermId> TermIdSet; typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index dcd3f1062..c5fe63ad6 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -20,7 +20,7 @@ #define __CVC4__BV_QUICK_CHECK_H #include <vector> -#include <ext/hash_map> +#include <unordered_set> #include "context/cdo.h" #include "expr/node.h" @@ -99,7 +99,7 @@ public: uint64_t computeAtomWeight(TNode atom, NodeSet& seen); void collectModelInfo(theory::TheoryModel* model, bool fullModel); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; + typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; vars_iterator beginVars(); vars_iterator endVars(); diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 3730ebc90..4b4103e44 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" +#include <unordered_map> +#include <unordered_set> + #include "theory/bv/bv_subtheory.h" -#include "theory/substitutions.h" #include "theory/bv/slicer.h" +#include "theory/substitutions.h" namespace CVC4 { namespace theory { @@ -60,8 +64,8 @@ class SubstitutionEx { {} }; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; @@ -104,9 +108,9 @@ struct WorklistElement { }; -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; -typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; class ExtractSkolemizer { @@ -123,7 +127,7 @@ class ExtractSkolemizer { ExtractList() : base(1), extracts() {} void addExtract(Extract& e); }; - typedef __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap; + typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap; context::Context d_emptyContext; VarExtractMap d_varToExtract; theory::SubstitutionMap* d_modelMap; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index c9fb81195..4bbe4327e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -18,6 +18,8 @@ #pragma once +#include <unordered_map> + #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_subtheory.h" @@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver { context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_modelCache; context::CDO<bool> d_validModelCache; diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 662f8835e..b416e019d 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" -#include "theory/bv/bv_subtheory.h" +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -31,9 +35,9 @@ class Base; * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { - typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; - typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; struct Statistics { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 37d3723ac..1123d15ae 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -19,10 +19,12 @@ #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H -#include "theory/bv/bv_subtheory.h" -#include "theory/bv/bv_inequality_graph.h" +#include <unordered_set> + #include "context/cdhashset.h" #include "expr/attribute.h" +#include "theory/bv/bv_inequality_graph.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -47,7 +49,7 @@ class InequalitySolver: public SubtheorySolver { InequalityGraph d_inequalityGraph; context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; context::CDO<bool> d_isComplete; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_ineqTerms; bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index a934cf045..93a83626e 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H +#include <unordered_map> + #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" @@ -26,7 +28,7 @@ namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; class BvToBoolPreprocessor { diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h index 935cbb7ed..e335c1339 100644 --- a/src/theory/bv/bvintropow2.h +++ b/src/theory/bv/bvintropow2.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include <vector> -#include <ext/hash_map> +#include <unordered_map> #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H #define __CVC4__THEORY__BV__BV_INTRO_POW_H @@ -36,7 +36,7 @@ public: static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess); private: - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache); }; diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index b594d5fec..dc8d333c4 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -20,7 +20,7 @@ #include <vector> #include <list> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" @@ -79,7 +79,7 @@ public: * UnionFind * */ -typedef __gnu_cxx::hash_set<TermId> TermSet; +typedef std::unordered_set<TermId> TermSet; typedef std::vector<TermId> Decomposition; struct ExtractTerm { @@ -226,9 +226,9 @@ public: }; class Slicer { - __gnu_cxx::hash_map<TermId, TNode> d_idToNode; - __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId; - __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; + std::unordered_map<TermId, TNode> d_idToNode; + std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId; + std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache; UnionFind d_unionFind; ExtractTerm registerTerm(TNode node); public: diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f8d3e6509..c20df35d5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -19,6 +19,9 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_H #define __CVC4__THEORY__BV__THEORY_BV_H +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" @@ -51,7 +54,7 @@ class TheoryBV : public Theory { context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; std::vector<SubtheorySolver*> d_subtheories; - __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; + std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: @@ -129,22 +132,22 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ - __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero; - __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero; + std::unordered_map<unsigned, Node> d_BVDivByZero; + std::unordered_map<unsigned, Node> d_BVRemByZero; - typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; + typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; // for ackermanization FunctionToArgs d_funcToArgs; CVC4::theory::SubstitutionMap d_funcToSkolem; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 46297cb68..61f072643 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -19,6 +19,9 @@ #pragma once +#include <unordered_map> +#include <unordered_set> + #include "theory/rewriter.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" @@ -922,7 +925,7 @@ struct Count { {} }; -inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { +inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { if(map.find(node) == map.end()) { Count c = neg? Count(0,1) : Count(1, 0); map[node] = c; @@ -945,7 +948,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant = utils::mkBitVectorOnes(size); @@ -974,7 +977,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1018,7 +1021,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; std::vector<Node> processingStack; processingStack.push_back(node); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; std::vector<Node> children; Kind kind = node.getKind(); @@ -1053,7 +1056,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant(size, (unsigned)0); @@ -1082,7 +1085,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1116,7 +1119,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl; - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant; bool const_set = false; @@ -1144,7 +1147,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { std::vector<Node> children; - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); unsigned true_count = 0; bool seen_false = false; for (; it != subterms.end(); ++it) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5bae1af4f..8b8d5e003 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -17,19 +17,22 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include <set> -#include <vector> #include <sstream> +#include <unordered_map> +#include <unordered_set> +#include <vector> + #include "expr/node_manager.h" namespace CVC4 { namespace theory { namespace bv { -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; namespace utils { @@ -505,11 +508,11 @@ inline T gcd(T a, T b) { return a; } -typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; +typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; bool isCoreTerm(TNode term, TNodeBoolMap& cache); bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; uint64_t numNodes(TNode node, NodeSet& seen); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index fd79e3fdc..a0333ed8b 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -19,7 +19,6 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H -#include <ext/hash_set> #include <iostream> #include <map> diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index e32fa1e71..6d81dbab0 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -1092,7 +1092,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) return true; } - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = d_leavesConstCache.find(e); if (it != d_leavesConstCache.end()) { return (*it).second; @@ -1173,7 +1173,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa Node ITESimplifier::getSimpVar(TypeNode t) { - std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; it = d_simpVars.find(t); if (it != d_simpVars.end()) { return (*it).second; @@ -1231,7 +1231,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) d_simpContextCache[c] = result; return result; } -typedef std::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){ if(visited.find(x) != visited.end()){ return; diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 29f4f7f1f..4aad9a3f0 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -22,8 +22,7 @@ #ifndef __CVC4__ITE_UTILITIES_H #define __CVC4__ITE_UTILITIES_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> #include <vector> #include "expr/node.h" @@ -80,7 +79,7 @@ public: size_t cache_size() const { return d_cache.size(); } private: - typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap; + typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap; NodeBoolMap d_cache; }; @@ -100,7 +99,7 @@ public: } void clear(); private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_reachCount; bool d_skipVariables; @@ -131,7 +130,7 @@ public: size_t cache_size() const; private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -158,7 +157,7 @@ private: std::vector<Node>* d_assertions; IncomingArcCounter d_incoming; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_compressed; void reset(); @@ -206,7 +205,7 @@ private: // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector<Node> NodeVec; - typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; + typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -249,23 +248,23 @@ private: return hash; } };/* struct ITESimplifier::NodePairHashFunction */ - typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; + typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; NodePairMap d_constantIteEqualsConstantCache; NodePairMap d_replaceOverCache; NodePairMap d_replaceOverTermIteCache; Node replaceOver(Node n, Node replaceWith, Node simpVar); Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); - std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache; + std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache; bool leavesAreConst(TNode e, theory::TheoryId tid); bool leavesAreConst(TNode e); NodePairMap d_simpConstCache; Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); - std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; Node getSimpVar(TypeNode t); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_simpContextCache; Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); @@ -314,7 +313,7 @@ private: Node d_true; Node d_false; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; class CareSetPtr; class CareSetPtrVal { diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4c1c93c17..5b714c2d3 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -17,7 +17,6 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H -#include <ext/hash_set> #include <iostream> #include <map> #include <vector> diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8d41c75d8..8597755c9 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -17,13 +17,10 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#include "util/hash.h" -#include "context/cdo.h" - -#include <ext/hash_set> #include <map> #include "context/cdlist.h" +#include "context/cdo.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 40a5b5849..f46b73b1c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -17,13 +17,12 @@ #ifndef __CVC4__THEORY__QUANT_UTIL_H #define __CVC4__THEORY__QUANT_UTIL_H -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" - -#include <ext/hash_set> #include <iostream> #include <map> +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 93390facb..ec5fc633d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -720,7 +720,7 @@ bool TermDb::reset( Theory::Effort effort ){ } } //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed - for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ + for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ Node n = *it; if( !ee->hasTerm( n ) ){ ee->addTerm( n ); @@ -2288,4 +2288,3 @@ Node TermDb::getQAttrQuantIdNumNode( Node q ) { }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f187e5989..4650cc5d4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -17,12 +17,14 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#include <map> +#include <unordered_set> + #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/quant_util.h" -#include <map> namespace CVC4 { namespace theory { @@ -194,9 +196,9 @@ private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_processed; + std::unordered_set< Node, NodeHashFunction > d_processed; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_iclosure_processed; + std::unordered_set< Node, NodeHashFunction > d_iclosure_processed; /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index d1412500e..9c621dbd6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,25 +19,19 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include <ext/hash_set> -#include <iostream> -#include <map> - #include "context/cdhashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/output_channel.h" #include "theory/theory.h" -#include "util/hash.h" +#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { -class TheoryEngine; - namespace theory { - namespace quantifiers { -class ModelEngine; -class InstantiationEngine; - class TheoryQuantifiers : public Theory { private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index faf14e0c7..fa1394f39 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1882,7 +1882,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r_best = r; } //now, make sure that no other member of the class is an instance - std::hash_map<TNode, Node, TNodeHashFunction> cache; + std::unordered_map<TNode, Node, TNodeHashFunction> cache; r_best = getInstance( r_best, eqc, cache ); //store that this representative was chosen at this point if( d_rep_score.find( r_best )==d_rep_score.end() ){ @@ -2001,7 +2001,7 @@ TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNo //helper functions -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){ +Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ if(cache.find(n) != cache.end()) { return cache[n]; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 92dfcdae5..7d8f5354b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,9 +17,9 @@ #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include <ext/hash_set> #include <iostream> #include <map> +#include <unordered_map> #include "context/cdchunk_list.h" #include "context/cdhashset.h" @@ -449,7 +449,7 @@ private: /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ - Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ int getRepScore( Node n, Node f, int index, TypeNode v_tn ); /** flatten representatives */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 27ab7615c..0c20c48a4 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) { } #ifdef CVC4_ASSERTIONS -static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; +static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { @@ -94,7 +94,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); if(s_rewriteStack == NULL) { - s_rewriteStack = new std::hash_set<Node, NodeHashFunction>(); + s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>(); } #endif diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 34c17a34c..beb5e946c 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -27,9 +27,9 @@ namespace sets { typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; -typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; +typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; -typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT; +typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl; @@ -240,7 +240,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } Node join_image_rel = join_image_term[0]; - std::hash_set< Node, NodeHashFunction > hasChecked; + std::unordered_set< Node, NodeHashFunction > hasChecked; Node join_image_rel_rep = getRepresentative( join_image_rel ); std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin(); MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep ); @@ -480,14 +480,14 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > if( tc_graph_it != (tc_it->second).end() ) { (tc_graph_it->second).insert( mem_rep_snd ); } else { - std::hash_set< Node, NodeHashFunction > sets; + std::unordered_set< Node, NodeHashFunction > sets; sets.insert( mem_rep_snd ); (tc_it->second)[mem_rep_fst] = sets; } } else { std::map< Node, Node > exp_map; - std::hash_set< Node, NodeHashFunction > sets; - std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map; + std::unordered_set< Node, NodeHashFunction > sets; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map; sets.insert( mem_rep_snd ); element_map[mem_rep_fst] = sets; d_tcr_tcGraph[tc_rel] = element_map; @@ -529,7 +529,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) ); if( tc_it != d_rRep_tcGraph.end() ) { bool isReachable = false; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ), getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable ); return isReachable; @@ -537,8 +537,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > return false; } - void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { if(hasSeen.find(start) == hasSeen.end()) { hasSeen.insert(start); } @@ -550,7 +550,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > isReachable = true; return; } else { - std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); while( set_it != pair_set_it->second.end() ) { // need to check if *set_it has been looked already @@ -565,7 +565,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) { std::map< Node, Node > rel_tc_graph_exps; - std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph; Node rel_rep = getRepresentative( tc_rel[0] ); Node tc_rel_rep = getRepresentative( tc_rel ); @@ -576,10 +576,10 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 )); Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 )); Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep ); - std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); if( rel_tc_graph_it == rel_tc_graph.end() ) { - std::hash_set< Node, NodeHashFunction > snd_elements; + std::unordered_set< Node, NodeHashFunction > snd_elements; snd_elements.insert( snd_element_rep ); rel_tc_graph[fst_element_rep] = snd_elements; rel_tc_graph_exps[tuple_rep] = exps[i]; @@ -596,13 +596,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } - void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) { - for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) { std::vector< Node > reasons; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() ); Node exp = rel_tc_graph_exps.find( tuple )->second; @@ -615,8 +615,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl; } - void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) { + void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) { Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); std::vector< Node > all_reasons( reasons ); @@ -646,7 +646,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > seen.insert( cur_node_rep ); TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); if( cur_set != tc_graph.end() ) { - for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); set_it != cur_set->second.end(); set_it++ ) { Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it ); std::vector< Node > new_reasons( reasons ); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 16770671a..eb97405dc 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -17,11 +17,13 @@ #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" -#include "context/cdhashset.h" +#include <unordered_set> + #include "context/cdchunk_list.h" +#include "context/cdhashset.h" #include "theory/sets/rels_utils.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -103,12 +105,12 @@ private: std::map< Node, Node > d_pending_facts; - std::hash_set< Node, NodeHashFunction > d_rel_nodes; + std::unordered_set< Node, NodeHashFunction > d_rel_nodes; std::map< Node, std::vector<Node> > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; /** Symbolic tuple variables that has been reduced to concrete ones */ - std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; + std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples; /** Mapping between relation and its member representatives */ std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; @@ -120,8 +122,8 @@ private: std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph; - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tcr_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; std::map< Node, std::vector< Node > > d_tc_lemmas_last; @@ -154,9 +156,9 @@ private: void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); void buildTCGraphForRel( Node tc_rel ); void doTCInference(); - void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); - void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ); + void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); + void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ); void composeMembersForRels( Node ); void computeMembersForBinOpRel( Node ); @@ -165,8 +167,8 @@ private: void computeMembersForJoinImageTerm( Node ); bool isTCReachable( Node mem_rep, Node tc_rel ); - void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); + void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); void addSharedTerm( TNode n ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3cce08398..8c3fe67d3 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -25,7 +25,7 @@ namespace theory { namespace sets { typedef std::set<TNode> Elements; -typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; +typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; struct FlattenedNodeTag {}; typedef expr::Attribute<FlattenedNodeTag, bool> flattened; @@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) return RewriteResponse(REWRITE_DONE, n); } - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 6b78a1698..5ca625751 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -17,6 +17,8 @@ #pragma once +#include <unordered_map> + #include "context/cdhashset.h" #include "expr/node.h" #include "theory/theory.h" @@ -43,7 +45,7 @@ private: IntStat d_statSharedTerms; // Needs to be a map from Nodes as after a backtrack they might not exist - typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; + typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; /** A map from atoms to a list of shared terms */ SharedTermsMap d_atomsToTerms; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a6618175..cca39a62e 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -19,9 +19,10 @@ #ifndef __CVC4__THEORY__SUBSTITUTIONS_H #define __CVC4__THEORY__SUBSTITUTIONS_H +//#include <algorithm> #include <utility> #include <vector> -#include <algorithm> +#include <unordered_map> #include "expr/node.h" #include "context/context.h" @@ -51,7 +52,7 @@ public: private: - typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache; /** The variables, in order of addition */ NodeMap d_substitutions; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 39cce27f9..2a84a7995 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -20,7 +20,7 @@ #include "context/context.h" #include "theory/shared_terms_database.h" -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { @@ -105,7 +105,7 @@ class SharedTermsVisitor { /** * Cache from preprocessing of atoms. */ - typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f010798cd..8509e84ab 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -220,8 +220,8 @@ void Theory::debugPrintFacts() const{ printFacts(DebugChannel.getStream()); } -std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ - std::hash_set<TNode, TNodeHashFunction> currentlyShared; +std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ + std::unordered_set<TNode, TNodeHashFunction> currentlyShared; for (shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i) { currentlyShared.insert (*i); diff --git a/src/theory/theory.h b/src/theory/theory.h index 82607a165..73102a6e2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include <ext/hash_set> #include <iosfwd> #include <map> #include <set> #include <string> +#include <unordered_set> #include "context/cdlist.h" #include "context/cdhashset.h" @@ -760,7 +760,7 @@ public: * This is a utility function for constructing a copy of the currently shared terms * in a queriable form. As this is */ - std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; + std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const; /** * This allows the theory to be queried for whether a literal, lit, is diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7369b7c1f..1023071dc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1645,7 +1645,7 @@ Node TheoryEngine::getExplanation(TNode node) { struct AtomsCollect { std::vector<TNode> d_atoms; - std::hash_set<TNode, TNodeHashFunction> d_visited; + std::unordered_set<TNode, TNodeHashFunction> d_visited; public: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 82283ef7b..408bff228 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -21,6 +21,7 @@ #include <deque> #include <set> +#include <unordered_map> #include <vector> #include <utility> @@ -189,8 +190,8 @@ class TheoryEngine { theory::TheoryEngineModelBuilder* d_curr_model_builder; bool d_aloc_curr_model_builder; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; /** * Cache for theory-preprocessing of assertions diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index b9a08e3ac..0f92f976e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -132,7 +132,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const { - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { return (*it).second; } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 126de1e46..c1c57795b 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -17,6 +17,9 @@ #ifndef __CVC4__THEORY__THEORY_MODEL_H #define __CVC4__THEORY__THEORY_MODEL_H +#include <unordered_map> +#include <unordered_set> + #include "smt/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" @@ -52,7 +55,7 @@ public: /** true/false nodes */ Node d_true; Node d_false; - mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache; + mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; public: /** comment stream to include in printing */ std::stringstream d_comment_str; @@ -140,8 +143,8 @@ public: */ class TypeSet { public: - typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; - typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; + typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; + typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; typedef TypeSetMap::iterator iterator; typedef TypeSetMap::const_iterator const_iterator; private: @@ -265,9 +268,9 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_normalizedCache; - typedef std::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::map< Node, Node > d_constantReps; /** process build model */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7c8e27575..5be32ab90 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -20,8 +20,8 @@ #pragma once #include <deque> -#include <ext/hash_map> #include <queue> +#include <unordered_map> #include <vector> #include "base/output.h" @@ -234,10 +234,10 @@ private: std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; /** Map from nodes to their ids */ - __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; + std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; /** Map from function applications to their ids */ - typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; + typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; /** * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives @@ -611,7 +611,7 @@ private: */ std::vector<TriggerTermSetRef> d_nodeIndividualTrigger; - typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; + typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; /** * A map from pairs of disequal terms, to the reason why we deduced they are disequal. diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index cffa367cf..8a1c30ba6 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -61,7 +61,7 @@ SymmetryBreaker::Template::Template() : } TNode SymmetryBreaker::Template::find(TNode n) { - hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); if(i == d_reps.end()) { return n; } else { @@ -400,8 +400,8 @@ void SymmetryBreaker::assertFormula(TNode phi) { break; } } - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; @@ -421,9 +421,9 @@ void SymmetryBreaker::assertFormula(TNode phi) { } if(!d_template.match(phi)) { // we hit a bad match, extract the partitions and reset the template - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition: " << (*i).first; diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index a814c670b..64ca41df2 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -46,6 +46,7 @@ #include <iostream> #include <list> +#include <unordered_map> #include <vector> #include "context/cdlist.h" @@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; NodeBuilder<> d_assertions; - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; - std::hash_map<TNode, TNode, TNodeHashFunction> d_reps; + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; + std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; TNode find(TNode n); bool matchRecursive(TNode t, TNode n); @@ -73,7 +74,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { public: Template(); bool match(TNode n); - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } Node assertions() { switch(d_assertions.getNumChildren()) { case 0: return Node::null(); @@ -91,7 +92,7 @@ public: typedef TNode Term; typedef std::list<Term> Terms; typedef std::set<Term> TermEq; - typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs; + typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs; private: @@ -113,7 +114,7 @@ private: Permutations d_permutations; Terms d_terms; Template d_template; - std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; + std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache; TermEqs d_termEqs; TermEqs d_termEqsOnly; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 783585f8f..6d4d96a87 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -300,7 +300,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { vector<TNode> workList; workList.push_back(n); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; while(!workList.empty()) { n = workList.back(); diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index a32dd076e..04c32f408 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -20,8 +20,10 @@ #ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H #define __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#include <vector> +#include <unordered_map> +#include <unordered_set> #include <utility> +#include <vector> #include "expr/node.h" #include "theory/substitutions.h" @@ -37,9 +39,9 @@ class UnconstrainedSimplifier { /** number of expressions eliminated due to unconstrained simplification */ IntStat d_numUnconstrainedElim; - typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; TNodeCountMap d_visited; TNodeMap d_visitedOnce; diff --git a/src/util/cache.h b/src/util/cache.h index 6f5bac8eb..38dc0fc99 100644 --- a/src/util/cache.h +++ b/src/util/cache.h @@ -21,8 +21,10 @@ #ifndef __CVC4__CACHE_H #define __CVC4__CACHE_H -#include <utility> #include <functional> +#include <unordered_map> +#include <utility> +#include <vector> namespace CVC4 { @@ -33,7 +35,7 @@ namespace CVC4 { */ template <class T, class U, class Hasher = std::hash<T> > class Cache { - typedef std::hash_map<T, U, Hasher> Map; + typedef std::unordered_map<T, U, Hasher> Map; Map d_map; std::vector<T> d_current; typename Map::iterator d_result; diff --git a/src/util/hash.h b/src/util/hash.h index af468e25b..b04fb8bb5 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -20,13 +20,10 @@ #ifndef __CVC4__HASH_H #define __CVC4__HASH_H -// in case it's not been declared as a namespace yet -namespace __gnu_cxx {} +#include <functional> +#include <string> -#include <ext/hash_map> -#include <ext/hash_set> - -namespace __gnu_cxx { +namespace std { #ifdef CVC4_NEED_HASH_UINT64_T // on some versions and architectures of GNU C++, we need a @@ -39,18 +36,10 @@ struct hash<uint64_t> { };/* struct hash<uint64_t> */ #endif /* CVC4_NEED_HASH_UINT64_T */ -}/* __gnu_cxx namespace */ - -// hackish: treat hash stuff as if it were in std namespace -namespace std { using namespace __gnu_cxx; } +}/* std namespace */ namespace CVC4 { -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash<const char*>()(str.c_str()); - } -};/* struct StringHashFunction */ template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> > struct PairHashFunction { diff --git a/src/util/hash.i b/src/util/hash.i index 470447fc3..f2f1e6652 100644 --- a/src/util/hash.i +++ b/src/util/hash.i @@ -2,6 +2,4 @@ #include "util/hash.h" %} -%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const; - %include "util/hash.h" diff --git a/src/util/proof.h b/src/util/proof.h index af68efa97..b34e4aed9 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -21,7 +21,7 @@ #define __CVC4__PROOF_H #include <iosfwd> -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { @@ -29,7 +29,7 @@ class Expr; class ProofLetCount; struct ExprHashFunction; -typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap; +typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap; class CVC4_PUBLIC Proof { public: diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 9915d480d..c32b42bad 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -17,6 +17,7 @@ #include "util/regexp.h" +#include <algorithm> #include <iomanip> #include <iostream> diff --git a/src/util/regexp.h b/src/util/regexp.h index beb0ee097..e7c8c5806 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -20,11 +20,13 @@ #ifndef __CVC4__REGEXP_H #define __CVC4__REGEXP_H -#include <vector> -#include <string> +#include <algorithm> +#include <cassert> +#include <functional> #include <set> #include <sstream> -#include <cassert> +#include <string> +#include <vector> #include "base/exception.h" #include "util/hash.h" @@ -333,7 +335,7 @@ namespace strings { struct CVC4_PUBLIC StringHashFunction { size_t operator()(const ::CVC4::String& s) const { - return __gnu_cxx::hash<const char*>()(s.toString().c_str()); + return std::hash<std::string>()(s.toString()); } };/* struct StringHashFunction */ diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 3094345bd..af1d9ab48 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -17,6 +17,8 @@ #include <cxxtest/TestSuite.h> +#include <unordered_set> + #include "expr/array_store_all.h" #include "expr/expr_manager.h" #include "expr/kind.h" @@ -252,7 +254,7 @@ std::cout<<"here\n"; void testArraysInfinite() { TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType())); - hash_set<Node, NodeHashFunction> elts; + unordered_set<Node, NodeHashFunction> elts; for(size_t i = 0; i < 1000; ++i) { TS_ASSERT( ! te.isFinished() ); Node elt = *te++; |