From 2bc4c351bbf89103577fa9f33ebb395f5d61826a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Oct 2010 20:20:24 +0000 Subject: Merge from cc-memout branch. Here are the main points * Add ContextMemoryAllocator allocator type, conforming to STL allocator requirements. * Extend the CDList<> template to take an allocator (defaults to std::allocator). * Add a specialized version of the CDList<> template (in src/context/cdlist_context_memory.h) that allocates a list in segments, in context memory. * Add "forward" headers -- cdlist_forward.h, cdmap_forward.h, and cdset_forward.h. Use these in public headers, and other places where you don't need the full header (just the forward-declaration). These types justify their own header (instead of just forward-declaring yourself), because they are complex templated types, with default template parameters, specializations, etc. * theory_engine.h no longer depends on individual theory headers. (Instead it forward-declares Theory implementations.) This is especially important now that theory .cpp files depend on TheoryEngine (to implement Theory::getValue()). Previously, any modification to any theory header file required *all* theories, and the engine, to be completely rebuilt. * Support memory cleanup for nontrivial CONSTANT kinds. This resolves an issue with arithmetic where memory leaked for each distinct Rational or Integer that was wrapped in a Node. --- src/expr/metakind_template.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'src/expr/metakind_template.h') diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index a336662c3..cb9730d34 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -275,6 +275,25 @@ ${metakind_constPrinters} } } +/** + * Cleanup to be performed when a NodeValue zombie is collected, and + * it has CONSTANT metakind. This calls the destructor for the underlying + * C++ type representing the constant value. See + * NodeManager::reclaimZombies() for more information. + * + * This doesn't support "non-inlined" NodeValues, which shouldn't need this + * kind of cleanup. + */ +inline void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constDeleters} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + inline unsigned getLowerBoundForKind(::CVC4::Kind k) { static const unsigned lbs[] = { 0, /* NULL_EXPR */ -- cgit v1.2.3