Merge from cc-memout branch. Here are the main points
authorMorgan Deters <mdeters@gmail.com>
Tue, 12 Oct 2010 20:20:24 +0000 (20:20 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 12 Oct 2010 20:20:24 +0000 (20:20 +0000)
commit2bc4c351bbf89103577fa9f33ebb395f5d61826a
tree37345ddbee75fc7405868afd3de8b7c2ffdd0fdc
parentec320b78deaaf31bdae1b8b048f66cfb1b3a4197
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.
27 files changed:
configure.ac
src/context/Makefile.am
src/context/cdlist.h
src/context/cdlist_context_memory.h [new file with mode: 0644]
src/context/cdlist_forward.h [new file with mode: 0644]
src/context/context_mm.cpp
src/context/context_mm.h
src/expr/metakind_template.h
src/expr/mkmetakind
src/expr/node_manager.cpp
src/expr/node_value.h
src/parser/smt/Smt.g
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/arith/arith_constants.h
src/theory/mktheoryof
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theoryof_table_template.h
src/theory/uf/morgan/theory_uf_morgan.cpp
src/theory/uf/morgan/theory_uf_morgan.h
src/util/congruence_closure.h
test/regress/regress0/uf/NEQ016_size5.smt [deleted file]
test/regress/regress3/Makefile.am
test/regress/regress3/NEQ016_size5.smt [new file with mode: 0644]
test/unit/Makefile.am
test/unit/context/cdlist_context_memory_black.h [new file with mode: 0644]