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

3 files changed, 16 insertions, 12 deletions

diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 0f8622cb8..a735cd46c 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -182,8 +182,6 @@ void Solver::cancelUntil(int level) {
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
     }
-    // Now, clear the TheoryEngine queue
-    proxy->clearAssertionQueues();
 }
 
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2ddbd24fc..d699153b2 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -77,6 +77,16 @@ public:
   CVC4_PUBLIC ~PropEngine();
 
   /**
+   * 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 (notably between
+   * PropEngine and Theory).  For now, there's nothing to do here in
+   * the PropEngine.
+   */
+  void shutdown() {
+  }
+
+  /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert
diff --git a/src/prop/sat.h b/src/prop/sat.h
index ec38bb019..f29436b97 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -77,8 +77,10 @@ public:
     inline size_t operator()(const SatLiteral& literal) const;
   };
 
-  inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context,
-            const Options* options);
+  inline SatSolver(PropEngine* propEngine,
+                   TheoryEngine* theoryEngine,
+                   context::Context* context,
+                   const Options* options);
 
   inline ~SatSolver();
 
@@ -93,8 +95,6 @@ public:
   inline void enqueueTheoryLiteral(const SatLiteral& l);
 
   inline void setCnfStream(CnfStream* cnfStream);
-
-  inline void clearAssertionQueues();
 };
 
 }/* CVC4::prop namespace */
@@ -135,7 +135,8 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
   return out;
 }
 
-size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+inline size_t
+SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
   return (size_t) minisat::toInt(literal);
 }
 
@@ -208,11 +209,6 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) {
   d_cnfStream = cnfStream;
 }
 
-
-void SatSolver::clearAssertionQueues() {
-  d_theoryEngine->clearAssertionQueues();
-}
-
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */