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

11 files changed, 229 insertions, 75 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 */
 
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.
    */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fb9be454a..f77e6cdf1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -23,12 +23,15 @@
 #include "theory/output_channel.h"
 #include "context/context.h"
 
-#include <queue>
+#include <deque>
 #include <list>
 
 #include <typeinfo>
 
 namespace CVC4 {
+
+class TheoryEngine;
+
 namespace theory {
 
 // rewrite cache support
@@ -50,13 +53,17 @@ class Theory {
 private:
 
   template <class T>
-  friend class TheoryImpl;
+  friend class ::CVC4::theory::TheoryImpl;
+
+  friend class ::CVC4::TheoryEngine;
 
   /**
    * Construct a Theory.
    */
   Theory(context::Context* ctxt, OutputChannel& out) throw() :
     d_context(ctxt),
+    d_facts(),
+    d_factsResetter(*this),
     d_out(&out) {
   }
 
@@ -65,12 +72,59 @@ private:
    */
   Theory();
 
+  /**
+   * The context for the Theory.
+   */
+  context::Context* d_context;
+
+  /**
+   * The assertFact() queue.
+   *
+   * This queue MUST be emptied by ANY call to check() at ANY effort
+   * level.  In debug builds, this is checked.  On backjump we clear
+   * the fact queue (see FactsResetter, below).
+   *
+   * These can safely be TNodes because the literal map maintained in
+   * the SAT solver keeps them live.  As an added benefit, if we have
+   * them as TNodes, dtors are cheap (optimized away?).
+   */
+  std::deque<TNode> d_facts;
+
+  /** Helper class to reset the fact queue on pop(). */
+  class FactsResetter : public context::ContextNotifyObj {
+    Theory& d_thy;
+
+  public:
+    FactsResetter(Theory& thy) :
+      context::ContextNotifyObj(thy.d_context),
+      d_thy(thy) {
+    }
+
+    void notify() {
+      d_thy.d_facts.clear();
+    }
+  } d_factsResetter;
+
+  friend class FactsResetter;
+
 protected:
 
   /**
-   * The output channel for the Theory.
+   * This is called at shutdown time by the TheoryEngine, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between PropEngine and Theory (based on what
+   * hard-links to Nodes are outstanding).  As the fact queue might be
+   * nonempty, we ensure here that it's clear.  If you overload this,
+   * you must make an explicit call here to the Theory implementation
+   * of this function too.
    */
-  context::Context* d_context;
+  virtual void shutdown() {
+    d_facts.clear();
+  }
+
+  context::Context* getContext() const {
+    return d_context;
+  }
 
   /**
    * The output channel for the Theory.
@@ -78,12 +132,11 @@ protected:
   OutputChannel* d_out;
 
   /**
-   * The assertFact() queue.
+   * Returns true if the assertFact queue is empty
    */
-  // FIXME CD: on backjump we clear the facts IFF the queue gets
-  // emptied on every DL.  In general I guess we need a CDQueue<>?
-  // Perhaps one that asserts it's empty at each push?
-  std::queue<Node> d_facts;
+  bool done() throw() {
+    return d_facts.empty();
+  }
 
   /**
    * Return whether a node is shared or not.  Used by setup().
@@ -91,10 +144,18 @@ protected:
   bool isShared(TNode n) throw();
 
   /**
-   * Returns true if the assertFact queue is empty
+   * Check whether a node is in the rewrite cache or not.
    */
-  bool done() throw() {
-    return d_facts.empty();
+  static bool inRewriteCache(TNode n) throw() {
+    return n.hasAttribute(RewriteCache());
+  }
+
+  /**
+   * Get the value of the rewrite cache (or Node::null()) if there is
+   * none).
+   */
+  static Node getRewriteCache(TNode n) throw() {
+    return n.getAttribute(RewriteCache());
   }
 
 public:
@@ -157,6 +218,13 @@ public:
   virtual void preRegisterTerm(TNode) = 0;
 
   /**
+   * Rewrite a term.  Done one time for a Node, ever.
+   */
+  virtual Node rewrite(TNode n) {
+    return n;
+  }
+
+  /**
    * Register a term.
    *
    * When get() is called to get the next thing off the theory queue,
@@ -174,20 +242,10 @@ public:
    */
   void assertFact(TNode n) {
     Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
-    d_facts.push(n);
+    d_facts.push_back(n);
   }
 
   /**
-   * Clear the assertion queue.
-   */
-  void clearAssertionQueue() {
-    while (d_facts.size() > 0) {
-      d_facts.pop();
-    }
-  }
-
-
-  /**
    * Check the current assignment's consistency.
    */
   virtual void check(Effort level = FULL_EFFORT) = 0;
@@ -306,7 +364,7 @@ Node TheoryImpl<T>::get() {
           "Theory::get() called with assertion queue empty!" );
 
   Node fact = d_facts.front();
-  d_facts.pop();
+  d_facts.pop_front();
 
   Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 49e4c2a88..2323a305b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -85,4 +85,44 @@ Node TheoryEngine::preprocess(TNode t) {
   return top;
 }
 
+Node TheoryEngine::rewrite(TNode in) {
+  if(inRewriteCache(in)) {
+    return getRewriteCache(in);
+  }
+
+  if(in.getKind() == kind::VARIABLE ||
+     in.getKind() == kind::SKOLEM) {
+    return in;
+  }
+
+  /*
+    theory::Theory* thy = theoryOf(in);
+    if(thy == NULL) {
+    Node out = rewriteBuiltins(in);
+    setRewriteCache(in, out);
+    return in;
+    } else {
+    Node out = thy->rewrite(in);
+    setRewriteCache(in, out);
+    return out;
+    }
+  */
+
+  if(in.getKind() == kind::EQUAL) {
+    Assert(in.getNumChildren() == 2);
+    if(in[0] == in[1]) {
+      Node out = NodeManager::currentNM()->mkNode(kind::TRUE);
+      //setRewriteCache(in, out);
+      return out;
+    }
+  } else {
+    Node out = rewriteChildren(in);
+    //setRewriteCache(in, out);
+    return out;
+  }
+
+  //setRewriteCache(in, in);
+  return in;
+}
+
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4d3a3c296..0b1afe748 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -96,7 +96,7 @@ class TheoryEngine {
   /**
    * Check whether a node is in the rewrite cache or not.
    */
-  bool inRewriteCache(TNode n) throw() {
+  static bool inRewriteCache(TNode n) throw() {
     return n.hasAttribute(theory::RewriteCache());
   }
 
@@ -104,39 +104,58 @@ class TheoryEngine {
    * Get the value of the rewrite cache (or Node::null()) if there is
    * none).
    */
-  Node getRewriteCache(TNode n) throw() {
+  static Node getRewriteCache(TNode n) throw() {
     return n.getAttribute(theory::RewriteCache());
   }
 
-  Node rewrite(TNode in) {
-    /*
-    Node out = theoryOf(in)->rewrite(in);
-    in.setAttribute(theory::RewriteCache(), out);
-    return out;
-    */
-    if(inRewriteCache(in)) {
-      return getRewriteCache(in);
-    } else if(in.getKind() == kind::VARIABLE) {
-      return in;
-    } else if(in.getKind() == kind::EQUAL) {
-      Assert(in.getNumChildren() == 2);
-      if(in[0] == in[1]) {
-        Node out = NodeManager::currentNM()->mkNode(kind::TRUE);
-        //in.setAttribute(theory::RewriteCache(), out);
-        return out;
-      }
-    } else {
-      NodeBuilder<> b(in.getKind());
-      for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
-        b << rewrite(*c);
-      }
-      Node out = b;
-      //in.setAttribute(theory::RewriteCache(), out);
-      return out;
+  /**
+   * Get the value of the rewrite cache (or Node::null()) if there is
+   * none).
+   */
+  static void setRewriteCache(TNode n, TNode v) throw() {
+    return n.setAttribute(theory::RewriteCache(), v);
+  }
+
+  /**
+   * This is the top rewrite entry point, called during preprocessing.
+   * It dispatches to the proper theories to rewrite the given Node.
+   */
+  Node rewrite(TNode in);
+
+  /**
+   * Convenience function to recurse through the children, rewriting,
+   * while leaving the Node's kind alone.
+   */
+  Node rewriteChildren(TNode in) {
+    NodeBuilder<> b(in.getKind());
+    for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
+      b << rewrite(*c);
     }
+    return Node(b);
+  }
 
-    //in.setAttribute(theory::RewriteCache(), in);
-    return in;
+  /**
+   * Rewrite Nodes with builtin kind (that is, those Nodes n for which
+   * theoryOf(n) == NULL).  The master list is in expr/builtin_kinds.
+   */
+  Node rewriteBuiltins(TNode in) {
+    switch(Kind k = in.getKind()) {
+    case kind::EQUAL:
+      return rewriteChildren(in);
+
+    case kind::ITE:
+      Unhandled(k);
+
+    case kind::SKOLEM:
+    case kind::VARIABLE:
+      return in;
+
+    case kind::TUPLE:
+      return rewriteChildren(in);
+
+    default:
+      Unhandled(k);
+    }
   }
 
 public:
@@ -161,6 +180,19 @@ public:
   }
 
   /**
+   * This is called at shutdown time by the SmtEngine, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between PropEngine and Theory.
+   */
+  void shutdown() {
+    d_bool.shutdown();
+    d_uf.shutdown();
+    d_arith.shutdown();
+    d_arrays.shutdown();
+    d_bv.shutdown();
+  }
+
+  /**
    * Get the theory associated to a given Node.
    *
    * @returns the theory, or NULL if the TNode is
@@ -241,13 +273,6 @@ public:
     return d_theoryOut.d_conflictNode;
   }
 
-  /**
-   * Clears the queues of the theories.
-   */
-  void clearAssertionQueues() {
-    d_uf.clearAssertionQueue();
-  }
-
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d6e1be9f2..6d949d6de 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -103,7 +103,7 @@ void TheoryUF::registerTerm(TNode n){
            "during backtracking");
   }else{
     //The attribute does not exist, so it is created and set
-    ecN = new (true) ECData(d_context, n);
+    ecN = new (true) ECData(getContext(), n);
     n.setAttribute(ECAttr(), ecN);
   }
 
@@ -134,7 +134,7 @@ void TheoryUF::registerTerm(TNode n){
         }
       }
 
-      ecChild->addPredecessor(n, d_context);
+      ecChild->addPredecessor(n, getContext());
     }
   }
   Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
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