From 20b3dabb4823ede8147a08a47f8d909980414bee Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 12 Mar 2010 19:41:04 +0000
Subject: * 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.
---
 src/theory/theory_engine.h | 97 +++++++++++++++++++++++++++++-----------------
 1 file changed, 61 insertions(+), 36 deletions(-)

(limited to 'src/theory/theory_engine.h')

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:
@@ -160,6 +179,19 @@ public:
     d_theoryOfTable.registerTheory(&d_bv);
   }
 
+  /**
+   * 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.
    *
@@ -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 */
-- 
cgit v1.2.3