Moved registration to theory engine

5 files changed, 96 insertions, 88 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 42d68efe5..ab94fbcc8 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -54,6 +54,12 @@ public:
   }
 
   /**
+   * Notify the OutputChannel that a new fact has been received by
+   * the theory.
+   */
+  virtual void newFact(TNode n) { }
+
+  /**
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index ba46e18e2..c93f26deb 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -26,83 +26,6 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
-Node Theory::get() {
-  Assert( !d_facts.empty(),
-          "Theory::get() called with assertion queue empty!" );
-
-  Node fact = d_facts.front();
-  d_facts.pop_front();
-
-  Debug("theory") << "Theory::get() => " << fact
-                  << "(" << d_facts.size() << " left)" << std::endl;
-
-  if(! fact.getAttribute(RegisteredAttr())) {
-    std::list<TNode> toReg;
-    toReg.push_back(fact);
-
-    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
-
-    /* Essentially this is doing a breadth-first numbering of
-     * non-registered subterms with children.  Any non-registered
-     * leaves are immediately registered. */
-    for(std::list<TNode>::iterator workp = toReg.begin();
-        workp != toReg.end();
-        ++workp) {
-
-      TNode n = *workp;
-
-      if(n.hasOperator()) {
-        TNode c = n.getOperator();
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-
-      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-        TNode c = *i;
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-    }
-
-    /* Now register the list of terms in reverse order.  Between this
-     * and the above registration of leaves, this should ensure that
-     * all subterms in the entire tree were registered in
-     * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
-        i != toReg.rend();
-        ++i) {
-
-      TNode n = *i;
-
-      /* Note that a shared TNode in the DAG rooted at "fact" could
-       * appear twice on the list, so we have to avoid hitting it
-       * twice. */
-      // FIXME when ExprSets are online, use one of those to avoid
-      // duplicates in the above?
-      if(! n.getAttribute(RegisteredAttr())) {
-        n.setAttribute(RegisteredAttr(), true);
-        registerTerm(n);
-      }
-    }
-  }
-
-  return fact;
-}
-
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
   case Theory::MIN_EFFORT:
diff --git a/src/theory/theory.h b/src/theory/theory.h
index ccc0a5f82..bcb2d011b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -214,16 +214,6 @@ protected:
     return d_facts.empty();
   }
 
-  /**
-   * Return whether a node is shared or not.  Used by setup().
-   */
-  bool isShared(TNode n) throw();
-
-  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-  struct Registered {};
-  /** The "registerTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
-
   /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
   struct PreRegistered {};
   /** The "preRegisterTerm()-has-been-called" flag on Nodes */
@@ -235,7 +225,16 @@ protected:
    *
    * @return the next atom in the assertFact() queue.
    */
-  Node get();
+  Node get() {
+    Assert( !d_facts.empty(),
+            "Theory::get() called with assertion queue empty!" );
+    Node fact = d_facts.front();
+    d_facts.pop_front();
+    Debug("theory") << "Theory::get() => " << fact
+                    << "(" << d_facts.size() << " left)" << std::endl;
+    d_out->newFact(fact);
+    return fact;
+  }
 
 public:
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c4dc1c508..839add67c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -41,6 +41,79 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
 
 }/* CVC4::theory namespace */
 
+void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
+  if(! fact.getAttribute(RegisteredAttr())) {
+    std::list<TNode> toReg;
+    toReg.push_back(fact);
+
+    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+
+    /* Essentially this is doing a breadth-first numbering of
+     * non-registered subterms with children.  Any non-registered
+     * leaves are immediately registered. */
+    for(std::list<TNode>::iterator workp = toReg.begin();
+        workp != toReg.end();
+        ++workp) {
+
+      TNode n = *workp;
+
+// I don't think we need to register operators @CB
+
+//       if(n.hasOperator()) {
+//         TNode c = n.getOperator();
+
+//         if(! c.getAttribute(RegisteredAttr())) {
+//           if(c.getNumChildren() == 0) {
+//             c.setAttribute(RegisteredAttr(), true);
+//             d_engine->theoryOf(c)->registerTerm(c);
+//           } else {
+//             toReg.push_back(c);
+//           }
+//         }
+//       }
+
+      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+        TNode c = *i;
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            d_engine->theoryOf(c)->registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+    }
+
+    /* Now register the list of terms in reverse order.  Between this
+     * and the above registration of leaves, this should ensure that
+     * all subterms in the entire tree were registered in
+     * reverse-topological order. */
+    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+        i != toReg.rend();
+        ++i) {
+
+      TNode n = *i;
+
+      /* Note that a shared TNode in the DAG rooted at "fact" could
+       * appear twice on the list, so we have to avoid hitting it
+       * twice. */
+      // FIXME when ExprSets are online, use one of those to avoid
+      // duplicates in the above?
+      // Actually, that doesn't work because you have to make sure 
+      // that the *last* occurrence is the one that gets processed first @CB
+      // This could be a big performance problem though because it requires
+      // traversing a DAG as a tree and that can really blow up @CB
+      if(! n.getAttribute(RegisteredAttr())) {
+        n.setAttribute(RegisteredAttr(), true);
+        d_engine->theoryOf(n)->registerTerm(n);
+      }
+    }
+  }
+}
+
+
 Theory* TheoryEngine::theoryOf(TNode n) {
   Kind k = n.getKind();
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0027903df..f467d0d8f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -54,6 +54,11 @@ class TheoryEngine {
   /** A table of Kinds to pointers to Theory */
   theory::TheoryOfTable d_theoryOfTable;
 
+  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+  struct Registered {};
+  /** The "registerTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
   /**
    * An output channel for Theory that passes messages
    * back to a TheoryEngine.
@@ -83,6 +88,8 @@ class TheoryEngine {
       d_explanationNode(context){
     }
 
+    void newFact(TNode n);
+
     void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
       Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
       d_conflictNode = conflictNode;