diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
commit | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (patch) | |
tree | 37345ddbee75fc7405868afd3de8b7c2ffdd0fdc /src/expr | |
parent | ec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (diff) |
Merge from cc-memout branch. Here are the main points
* Add ContextMemoryAllocator<T> allocator type, conforming to
STL allocator requirements.
* Extend the CDList<> template to take an allocator (defaults
to std::allocator<T>).
* 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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/metakind_template.h | 19 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 9 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 13 | ||||
-rw-r--r-- | src/expr/node_value.h | 10 |
4 files changed, 49 insertions, 2 deletions
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 */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 351893feb..c68ba59cd 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -44,6 +44,7 @@ metakind_constantMaps= metakind_compares= metakind_constHashes= metakind_constPrinters= +metakind_constDeleters= metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= @@ -192,6 +193,13 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { out << nv->getConst< $2 >(); break; " + cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'` + metakind_constDeleters="${metakind_constDeleters} + case kind::$1: +#line $lineno \"$kf\" + std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children)); + break; +" } function registerOperatorToKind { @@ -301,6 +309,7 @@ for var in \ metakind_compares \ metakind_constHashes \ metakind_constPrinters \ + metakind_constDeleters \ metakind_ubchildren \ metakind_lbchildren \ metakind_operatorKinds; do diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5c24699b8..4e872ad5c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -164,7 +164,8 @@ void NodeManager::reclaimZombies() { << " [" << nv->d_id << "]: " << *nv << "\n"; // remove from the pool - if(nv->getMetaKind() != kind::metakind::VARIABLE) { + kind::MetaKind mk = nv->getMetaKind(); + if(mk != kind::metakind::VARIABLE) { poolRemove(nv); } @@ -179,6 +180,16 @@ void NodeManager::reclaimZombies() { // decr ref counts of children nv->decrRefCounts(); + if(mk == kind::metakind::CONSTANT) { + // Destroy (call the destructor for) the C++ type representing + // the constant in this NodeValue. This is needed for + // e.g. CVC4::Rational, since it has a gmp internal + // representation that mallocs memory and should be cleaned + // up. (This won't delete a pointer value if used as a + // constant, but then, you should probably use a smart-pointer + // type for a constant payload.) + kind::metakind::deleteNodeValueConstant(nv); + } free(nv); } } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index bc592b4e5..a42f39e15 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -46,6 +46,10 @@ class PlusNodeBuilder; class MultNodeBuilder; class NodeManager; +namespace expr { + class NodeValue; +} + namespace kind { namespace metakind { template < ::CVC4::Kind k, bool pool > @@ -53,6 +57,8 @@ namespace kind { struct NodeValueCompare; struct NodeValueConstPrinter; + + void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv); }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -110,11 +116,13 @@ class NodeValue { friend class ::CVC4::NodeManager; template <Kind k, bool pool> - friend struct ::CVC4::kind::metakind::NodeValueConstCompare; + friend struct ::CVC4::kind::metakind::NodeValueConstCompare; friend struct ::CVC4::kind::metakind::NodeValueCompare; friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; + friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv); + void inc(); void dec(); |