diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/congruence_closure.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index cc18a3305..db9d5bc65 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -28,9 +28,11 @@ #include "expr/node_manager.h" #include "expr/node.h" +#include "context/context_mm.h" +#include "context/cdo.h" #include "context/cdmap.h" #include "context/cdset.h" -#include "context/cdlist.h" +#include "context/cdlist_context_memory.h" #include "util/exception.h" namespace CVC4 { @@ -102,9 +104,9 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap; - typedef context::CDList<Node> ClassList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList; typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists; - typedef context::CDList<Node> UseList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList; typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists; typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap; @@ -348,7 +350,8 @@ private: UseLists::iterator usei = d_useList.find(of); UseList* ul; if(usei == d_useList.end()) { - ul = new(d_context->getCMM()) UseList(true, d_context); + ul = new(d_context->getCMM()) UseList(true, d_context, false, + context::ContextMemoryAllocator<TNode>(d_context->getCMM())); d_useList.insertDataFromContextMemory(of, ul); } else { ul = (*usei).second; @@ -549,7 +552,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { ClassLists::iterator cl_bpi = d_classList.find(bp); ClassList* cl_bp; if(cl_bpi == d_classList.end()) { - cl_bp = new(d_context->getCMM()) ClassList(true, d_context); + cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false, + context::ContextMemoryAllocator<TNode>(d_context->getCMM())); d_classList.insertDataFromContextMemory(bp, cl_bp); Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl; } else { |