diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
| commit | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (patch) | |
| tree | ceea43e3d37525038bed10b115c73a8aa08ce68d /src/smt/smt_engine.cpp | |
| parent | de0160112edbed8ce9b62bf87172ae2f0e99a013 (diff) | |
This fixes regressions at levels >= 1 which were failing
* implement zombification and garbage collection of NodeValues
(but GC not turned on yet)
* implement removal of key nodes from all attribute tables
* audit NodeBuilder and fix memory leaks and improper reference-count
management. This is in many places a re-write. Clearly documented
invariants on NodeBuilder state. (Closes Bug 38)
* created a "BackedNodeBuilder" that can be used to construct
NodeBuilders with a stack-based backing store for a size that's not
a compile-time constant.
* NodeValues no longer depend on Node for toStream()'ing
* make unit test-building "silent" with --enable-silent-rules
* (Makefile.am, Makefile.builds.in) fix top-level build system so that
"make regressN" works with unbuilt/out-of-date source trees in the
expected way.
* (various) code cleanup, documentation, formatting
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8def3e279..6e3a1b801 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -10,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The main entry point into the CVC4 library's SMT interface. **/ #include "smt/smt_engine.h" @@ -67,6 +68,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_exprManager(em), d_nodeManager(em->getNodeManager()), d_options(opts) { + NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; d_theoryEngine = new TheoryEngine(this, d_ctxt); |