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, 19 insertions, 0 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 */