* 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.

2 files changed, 10 insertions, 1 deletions

diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index 9b6101a2a..06ea283a8 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -26,7 +26,7 @@ DecisionEngine::~DecisionEngine() {
  * virtual in the final design (?)
  */
 Node DecisionEngine::nextDecision() {
-  Unreachable();
+  Unimplemented();
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index ac9fc5ffd..fd757b734 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -41,6 +41,15 @@ public:
    */
   virtual Node nextDecision();// = 0
 
+  /**
+   * This is called by SmtEngine, at shutdown time, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between some parts of the system.  For now,
+   * there's nothing to do here in the DecisionEngine.
+   */
+  virtual void shutdown() {
+  }
+
   // TODO: design decision: decision engine should be notified of
   // propagated lits, and also why(?) (so that it can make decisions
   // based on the utility of various theories and various theory