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