summaryrefslogtreecommitdiff
path: root/test/unit/theory/theory_black.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-12 20:20:24 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-12 20:20:24 +0000
commit2bc4c351bbf89103577fa9f33ebb395f5d61826a (patch)
tree37345ddbee75fc7405868afd3de8b7c2ffdd0fdc /test/unit/theory/theory_black.h
parentec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (diff)
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.
Diffstat (limited to 'test/unit/theory/theory_black.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback