diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-12 19:41:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-12 19:41:04 +0000 |
commit | 20b3dabb4823ede8147a08a47f8d909980414bee (patch) | |
tree | 6d6ea617bef8d840de8f8ff737e00acadb6675f9 /src/smt | |
parent | 3cf73e344987c2449943ca3a97054565eb9d5726 (diff) |
* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
DecisionEngine, and Theory. These are triggered from the SmtEngine
dtor before the other engines are deleted. This is important
because of potential issues with outstanding TNodes in Theory
implementations (which fail if the destruction is done in the wrong
order, in certain cases).
* Favor "FactQueueResetter" instead of clearAssertionQueues() for
resetting facts queue in Theory implementations.
* Better theory-rewriting code.
* Minor cleanups.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 10 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 8 |
2 files changed, 18 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e97adb1d2..c00112cd0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,13 +70,23 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_options(opts) { NodeManagerScope nms(d_nodeManager); + d_decisionEngine = new DecisionEngine; d_theoryEngine = new TheoryEngine(this, d_ctxt); d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); } +void SmtEngine::shutdown() { + d_propEngine->shutdown(); + d_theoryEngine->shutdown(); + d_decisionEngine->shutdown(); +} + SmtEngine::~SmtEngine() { NodeManagerScope nms(d_nodeManager); + + shutdown(); + delete d_propEngine; delete d_theoryEngine; delete d_decisionEngine; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 36cb8746c..4836b282e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -146,6 +146,14 @@ private: // smt_engine.cpp. /** + * This is called by the destructor, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + + /** * Full check of consistency in current context. Returns true iff * consistent. */ |