Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).

5 files changed, 170 insertions, 123 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7a8ebb85c..593274281 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -138,7 +138,7 @@ void TheoryBV::check(Effort e) {
       normalization.assumptions.push_back(assumptions);
 
       BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl;
-      BVDebug("bitvector") << "       assumptions   " << setToString(assumptions) << std::endl;
+      BVDebug("bitvector") << "       assumptions   " << utils::setToString(assumptions) << std::endl;
 
 
       BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
@@ -234,7 +234,7 @@ void TheoryBV::explain(TNode node) {
   std::set<TNode> assumptions;
   for (unsigned i = 0; i < vec.size(); ++ i) {
     BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl;
-    BVDebug("bitvector") << "       assumptions   " << setToString(d_normalization[equality]->assumptions[i]) << std::endl;
+    BVDebug("bitvector") << "       assumptions   " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl;
     assumptions.insert(vec[i].begin(), vec[i].end());
   }
   d_out->explanation(utils::mkConjunction(assumptions));
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index a9722690b..44aed8b17 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -54,12 +54,6 @@ 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.h b/src/theory/theory.h
index 1d8797d1f..2256c4462 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -137,7 +137,6 @@ protected:
     d_factsHead = d_factsHead + 1;
     Trace("theory") << "Theory::get() => " << fact
                     << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
-    d_out->newFact(fact);
     return fact;
   }
 
@@ -311,19 +310,6 @@ public:
   virtual void preRegisterTerm(TNode) { }
 
   /**
-   * Register a term.
-   *
-   * When get() is called to get the next thing off the theory queue,
-   * setup() is called on its subterms (in TheoryEngine).  Then setup()
-   * is called on this node.
-   *
-   * This is done in a "context escape" -- that is, at context level 0.
-   * setup() MUST NOT MODIFY context-dependent objects that it hasn't
-   * itself just created.
-   */
-  virtual void registerTerm(TNode) { }
-
-  /**
    * Assert a fact in the current context.
    */
   void assertFact(TNode node) {
@@ -486,6 +472,35 @@ public:
    */
   virtual std::string identify() const = 0;
 
+  /** A set of theories */
+  typedef uint32_t Set;
+
+  /** Add the theory to the set. If no set specified, just returns a singleton set */
+  static inline Set setInsert(TheoryId theory, Set set = 0) {
+    return set | (1 << theory);
+  }
+
+  /** Check if the set containt the theory */
+  static inline bool setContains(TheoryId theory, Set set) {
+    return set & (1 << theory);
+  }
+
+  static inline Set setUnion(Set a, Set b) {
+    return a | b;
+  }
+
+  static inline std::string setToString(theory::Theory::Set theorySet) {
+    std::stringstream ss;
+    ss << "[";
+    for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
+      if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
+        ss << (theory::TheoryId) theoryId << " ";
+      }
+    }
+    ss << "]";
+    return ss.str();
+  }
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 833c03e2f..7447726b4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -37,43 +37,23 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 
-/** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-struct RegisteredAttrTag {};
-/** The "registerTerm()-has-been-called" flag on Nodes */
-typedef expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr;
-
 /** Tag for the "preregisterTerm()-has-benn-called" flag on nodes */
 struct PreRegisteredAttrTag {};
 /** The "preregisterTerm()-has-been-called" flag on Nodes */
-typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegisteredAttr;
-
-void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
-  TimerStat::CodeTimer codeTimer(d_newFactTimer);
-
-  if (fact.getKind() == kind::NOT) {
-    // No need to register negations - only atoms
-    fact = fact[0];
-  }
-
-  if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) && d_engine->d_needRegistration) {
-    RegisterVisitor visitor(*d_engine);
-    NodeVisitor<RegisterVisitor, RegisteredAttr>::run(visitor, fact);
-  }
-}
+typedef expr::Attribute<PreRegisteredAttrTag, Theory::Set> PreRegisteredAttr;
 
 TheoryEngine::TheoryEngine(context::Context* ctxt) :
   d_propEngine(NULL),
   d_context(ctxt),
   d_activeTheories(0),
-  d_needRegistration(false),
   d_theoryOut(this, ctxt),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
-  d_statistics() {
+  d_statistics(),
+  d_preRegistrationVisitor(*this) {
 
   for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
     d_theoryTable[theoryId] = NULL;
-    d_theoryIsActive[theoryId] = false;
   }
 
   Rewriter::init();
@@ -107,8 +87,7 @@ struct preregister_stack_element {
 };/* struct preprocess_stack_element */
 
 void TheoryEngine::preRegister(TNode preprocessed) {
-  PreRegisterVisitor visitor(*this);
-  NodeVisitor<PreRegisterVisitor, PreRegisteredAttr>::run(visitor, preprocessed);
+  NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
 }
 
 /**
@@ -123,7 +102,7 @@ void TheoryEngine::check(theory::Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
+  if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
      if (d_theoryOut.d_inConflict) { \
        return; \
@@ -144,7 +123,7 @@ void TheoryEngine::propagate() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \
+  if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \
       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
   }
 
@@ -205,7 +184,7 @@ void TheoryEngine::notifyRestart() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \
+  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \
   }
 
@@ -233,22 +212,6 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
   CVC4_FOR_EACH_THEORY;
 }
 
-bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
-  switch(th) {
-  // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  case THEORY: \
-    return theory::TheoryTraits<THEORY>::hasRegisterTerm;
-
-    CVC4_FOR_EACH_THEORY
-  default:
-    Unhandled(th);
-  }
-}
-
 theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c472a1c41..ea3fe95c1 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -68,19 +68,7 @@ class TheoryEngine {
    * runs (no sharing), can reduce the cost of walking the DAG on
    * registration, etc.
    */
-  bool d_theoryIsActive[theory::THEORY_LAST];
-
-  /**
-   * The count of active theories in the d_theoryIsActive bitmap.
-   */
-  size_t d_activeTheories;
-
-  /**
-   * Need the registration infrastructure when theory sharing is on
-   * (>=2 active theories) or when the sole active theory has
-   * requested it.
-   */
-  bool d_needRegistration;
+  theory::Theory::Set d_activeTheories;
 
   /**
    * Cache from proprocessing of atoms.
@@ -108,11 +96,6 @@ class TheoryEngine {
      */
     std::vector<TNode> d_propagatedLiterals;
 
-    /** Time spent in newFact() (largely spent doing term registration) */
-    KEEP_STATISTIC(TimerStat,
-                   d_newFactTimer,
-                   "theory::newFactTimer");
-
     /**
      * Check if the node is in conflict for debug purposes
      */
@@ -150,7 +133,7 @@ class TheoryEngine {
 
       // Construct the lemma (note that no CNF caching should happen as all the literals already exists)
       Assert(isProperConflict(conflictNode));
-      d_engine->newLemma(conflictNode, true, true);
+      d_engine->newLemma(conflictNode, true, false);
 
       if(safe) {
         throw theory::Interrupted();
@@ -214,24 +197,16 @@ class TheoryEngine {
   /**
    * Mark a theory active if it's not already.
    */
-  void markActive(theory::TheoryId th) {
-    if(!d_theoryIsActive[th]) {
-      d_theoryIsActive[th] = true;
-      if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) {
-        if(++d_activeTheories == 1) {
-          // theory requests registration
-          d_needRegistration = hasRegisterTerm(th);
-        } else {
-          // need it for sharing
-          d_needRegistration = true;
-        }
-      }
-      Notice() << "Theory " << th << " has been activated (registration is "
-               << (d_needRegistration ? "on" : "off") << ")." << std::endl;
-    }
+  void markActive(theory::Theory::Set theories) {
+    d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories);
   }
 
-  bool hasRegisterTerm(theory::TheoryId th) const;
+  /**
+   * Is the theory active.
+   */
+  bool isActive(theory::TheoryId theory) {
+    return theory::Theory::setContains(theory, d_activeTheories);
+  }
 
   /** The logic of the problem */
   std::string d_logic;
@@ -321,6 +296,16 @@ public:
   }
 
   /**
+   * Get the theory associated to a the given theory id.
+   *
+   * @returns the theory, or NULL if the TNode is
+   * of built-in type.
+   */
+  inline theory::Theory* theoryOf(theory::TheoryId theoryId) {
+    return d_theoryTable[theoryId];
+  }
+
+  /**
    * Solve the given literal with a theory that owns it.
    */
   theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut);
@@ -453,40 +438,130 @@ private:
     /** The engine */
     TheoryEngine& d_engine;
 
+    /**
+     * Cache from proprocessing of atoms.
+     */
+    typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+    TNodeVisitedMap d_visited;
+
+    /**
+     * All the theories of the visitation.
+     */
+    theory::Theory::Set d_theories;
+
+    std::string toString() const {
+      std::stringstream ss;
+      TNodeVisitedMap::const_iterator it = d_visited.begin();
+      for (; it != d_visited.end(); ++ it) {
+        ss << it->first << ": " << theory::Theory::setToString(it->second) << std::endl;
+      }
+      return ss.str();
+    }
+
   public:
 
-    PreRegisterVisitor(TheoryEngine& engine): d_engine(engine) {}
+    PreRegisterVisitor(TheoryEngine& engine): d_engine(engine), d_theories(0) {}
 
-    void operator () (TNode current) {
-      // Get the theory of the term and pre-register it with the owning theory
-      theory::TheoryId currentTheoryId = theory::Theory::theoryOf(current);
-      Debug("register") << "preregistering " << current << " with " << currentTheoryId << std::endl;
-      d_engine.markActive(currentTheoryId);
-      theory::Theory* currentTheory = d_engine.theoryOf(current);
-      currentTheory->preRegisterTerm(current);
+    bool alreadyVisited(TNode current, TNode parent) {
+
+      Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => ";
+
+      using namespace theory;
+
+      TNodeVisitedMap::iterator find = d_visited.find(current);
+
+      // If node is not visited at all, just return false
+      if (find == d_visited.end()) {
+        Debug("register::internal") << "1:false" << std::endl;
+        return false;
+      }
+
+      TheoryId currentTheoryId = Theory::theoryOf(current);
+      if (Theory::setContains(currentTheoryId, find->second)) {
+        // The current theory has already visited it, so now it depends on the parent
+        TheoryId parentTheoryId = Theory::theoryOf(parent);
+        if (parentTheoryId == currentTheoryId) {
+          // If it's the same theory, we've visited it already
+          Debug("register::internal") << "2:true" << std::endl;
+          return true;
+        }
+        // If not the same theory, we might have visited it, just check
+        Debug("register::internal") << (Theory::setContains(parentTheoryId, find->second) ? "3:true" : "3:false") << std::endl;
+        return Theory::setContains(parentTheoryId, find->second);
+      } else {
+        // If the current theory is not registered, it still needs to be visited
+        Debug("register::internal") << "4:false" << std::endl;
+        return false;
+      }
     }
-  };
 
-  /**
-   * Visitor that calls the apropriate theory to preregister the term.
-   */
-  class RegisterVisitor {
+    void visit(TNode current, TNode parent) {
 
-    /** The engine */
-    TheoryEngine& d_engine;
+      Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
+      Debug("register::internal") << toString() << std::endl;
 
-  public:
+      using namespace theory;
+
+      // Get the theories of the terms
+      TheoryId currentTheoryId = Theory::theoryOf(current);
+      TheoryId parentTheoryId  = Theory::theoryOf(parent);
+
+      if (currentTheoryId == parentTheoryId) {
+        // If it's the same theory we just add it
+        TNodeVisitedMap::iterator find = d_visited.find(current);
+        if (find == d_visited.end()) {
+          d_visited[current] = Theory::setInsert(currentTheoryId);
+        } else {
+          find->second = Theory::setInsert(currentTheoryId, find->second);
+        }
+        // Visit it
+        d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+        // Mark the theory as active
+        d_theories = Theory::setInsert(currentTheoryId, d_theories);
+      } else {
+        // If two theories, one might have visited it already
+        // If it's the same theory we just add it
+        TNodeVisitedMap::iterator find = d_visited.find(current);
+        if (find == d_visited.end()) {
+          // If not in the map at all, we just add both
+          d_visited[current] = Theory::setInsert(parentTheoryId, Theory::setInsert(currentTheoryId));
+          // And visit both
+          d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+          d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current);
+          // Mark both theories as active
+          d_theories = Theory::setInsert(currentTheoryId, d_theories);
+          d_theories = Theory::setInsert(parentTheoryId, d_theories);
+        } else {
+          if (!Theory::setContains(currentTheoryId, find->second)) {
+            find->second = Theory::setInsert(currentTheoryId, find->second);
+            d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+            d_theories = Theory::setInsert(currentTheoryId, d_theories);
+          }
+          if (!Theory::setContains(parentTheoryId, find->second)) {
+            find->second = Theory::setInsert(parentTheoryId, find->second);
+            d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current);
+            d_theories = Theory::setInsert(parentTheoryId, d_theories);
+          }
+        }
+      }
 
-    RegisterVisitor(TheoryEngine& engine): d_engine(engine) {}
+      Assert(d_visited.find(current) != d_visited.end());
+      Assert(alreadyVisited(current, parent));
+    }
 
-    void operator () (TNode current) {
-      // Register this node to it's theory
-      theory::Theory* currentTheory = d_engine.theoryOf(current);
-      Debug("register") << "registering " << current << " with " << currentTheory->getId() << std::endl;
-      currentTheory->registerTerm(current);
+    void start(TNode node) {
+      d_theories = 0;
     }
+
+    void done(TNode node) {
+      d_engine.markActive(d_theories);
+    }
+
   };
 
+  /** Default visitor for pre-registration */
+  PreRegisterVisitor d_preRegistrationVisitor;
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */