diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
commit | 068107e1d1f705eb9054b4309a26236230687d80 (patch) | |
tree | 4c422f3efd6a8319abe426c518f9d2feb7ab5a6d /src/theory/arrays | |
parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) |
CDMap -> CDHashMap
CDSet -> CDHashSet
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 10 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index fcc45bbd5..d1c435b48 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -41,7 +41,7 @@ #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #include "util/backtrackable.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "util/stats.h" #include "util/ntuple.h" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d699617e2..fcb6ee382 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -152,8 +152,8 @@ private: typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc; - typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap; - typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists; + typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap; + typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists; typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap; @@ -174,7 +174,7 @@ private: /** List of disequalities needed to construct explanations for propagated * row lemmas */ - context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations; + context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations; /** * stores the conflicting disequality (still need to call construct @@ -447,9 +447,9 @@ public: void propagate(Effort e) { - Trace("arrays-prop")<<"Propagating \n"; + // Trace("arrays-prop")<<"Propagating \n"; - context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); + // context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); /* for(; it!= d_prop_queue.end(); it++) { TNode eq = *it; |