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 /src/expr/node.h | |
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.
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 42 |
1 files changed, 21 insertions, 21 deletions
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; |