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/theory/arrays | |
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/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.h | 5 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 9 | ||||
-rw-r--r-- | src/theory/arrays/union_find.h | 4 |
6 files changed, 20 insertions, 16 deletions
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. |