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.

1 files changed, 12 insertions, 1 deletions

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);
     }
   }