Moved registration to theory engine

1 files changed, 7 insertions, 0 deletions

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;