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, 9 insertions, 0 deletions

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