diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
| commit | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (patch) | |
| tree | 37345ddbee75fc7405868afd3de8b7c2ffdd0fdc /src/smt | |
| parent | ec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (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 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 594efcc35..e3c8c584c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,6 +26,7 @@ #include "smt/no_such_function_exception.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdset.h" #include "expr/expr.h" #include "expr/command.h" #include "expr/node_builder.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d6940f09f..a3116dfa9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -27,6 +27,7 @@ #include "expr/expr_manager.h" #include "context/cdmap_forward.h" #include "context/cdset_forward.h" +#include "context/cdlist_forward.h" #include "util/result.h" #include "util/model.h" #include "util/sexpr.h" @@ -52,7 +53,6 @@ class DecisionEngine; namespace context { class Context; - template <class T> class CDList; }/* CVC4::context namespace */ namespace prop { |