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, 11 insertions, 5 deletions

diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
index 27abd8873..98a202207 100644
--- a/src/theory/arith/arith_constants.h
+++ b/src/theory/arith/arith_constants.h
@@ -31,7 +31,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class ArithConstants{
+class ArithConstants {
 public:
   Rational d_ZERO;
   Rational d_ONE;
@@ -52,10 +52,16 @@ public:
     d_ONE_NODE(nm->mkConst(d_ONE)),
     d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
   {}
-};
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+  ~ArithConstants() {
+    d_ZERO_NODE = Node::null();
+    d_ONE_NODE = Node::null();
+    d_NEGATIVE_ONE_NODE = Node::null();
+  }
+};/* class ArithConstants */
+
+}/* namespace CVC4::theory::arith */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
 
 #endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */