Refactor term registration visitors (#5875)

This refactors the term registration visitors (PreRegisterVisitor and SharedTermsVisitor), which are responsible for calling Theory::preRegisterTerm and Theory::addSharedTerm.

The purpose of this PR is to resolve a subtle bug in the implementation of PreRegisterVisitor (see explanation below), and to improve performance in particular on the Facebook benchmarks (where preregistering terms is currently 25-35% of runtime on certain challenge benchmarks).

This PR makes it so that that SharedTermsVisitor now subsumes PreRegisterVisitor and should be run when sharing is enabled only. Previously, we ran both PreRegisterVisitor and SharedTermsVisitor, and moreover the former misclassified when a literal had multiple theories since the d_theories field of PreRegisterVisitor is never reset. This meant we would consider a literal to have multiple theories as soon as we saw any literal that had multipleTheories. After this PR, we run SharedTermsVisitor only which also handles calling preRegisterTerm, since it has the ability to anyways (it computes the same information as PreRegisterVisitor regarding which theories care about a term).

The refactoring merges the blocks of code that were copy and pasted in term_registration_visitor.cpp and makes them more optimal, by reducing our calls to Theory::theoryOf.

FYI @barrettcw

1 files changed, 132 insertions, 208 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index b4ad87f1e..82463367e 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -18,9 +18,9 @@
 #include "options/quantifiers_options.h"
 #include "theory/theory_engine.h"
 
-using namespace std;
-using namespace CVC4;
-using namespace theory;
+using namespace CVC4::theory;
+
+namespace CVC4 {
 
 std::string PreRegisterVisitor::toString() const {
   std::stringstream ss;
@@ -32,6 +32,47 @@ std::string PreRegisterVisitor::toString() const {
   return ss.str();
 }
 
+/**
+ * Return true if we already visited the term current with the given parent,
+ * assuming that the set of theories in visitedTheories has already processed
+ * current. This method is used by PreRegisterVisitor and SharedTermsVisitor
+ * below.
+ */
+bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent)
+{
+  TheoryId currentTheoryId = Theory::theoryOf(current);
+  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
+  {
+    // current theory not visited, return false
+    return false;
+  }
+
+  if (current == parent)
+  {
+    // top-level and current visited, return true
+    return true;
+  }
+
+  // The current theory has already visited it, so now it depends on the parent
+  // and the type
+  TheoryId parentTheoryId = Theory::theoryOf(parent);
+  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
+  {
+    // parent theory not visited, return false
+    return false;
+  }
+
+  // do we need to consider the type?
+  TypeNode type = current.getType();
+  if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite())
+  {
+    // current and parent are the same theory, and we are infinite, return true
+    return true;
+  }
+  TheoryId typeTheoryId = Theory::theoryOf(type);
+  return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
+}
+
 bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
@@ -47,62 +88,16 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
     Debug("register::internal") << "quantifier:true" << std::endl;
     return true;
   }
-
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId = Theory::theoryOf(parent);
-
-  d_theories = TheoryIdSetUtil::setInsert(currentTheoryId, d_theories);
-  d_theories = TheoryIdSetUtil::setInsert(parentTheoryId, d_theories);
-
-  // Should we use the theory of the type
-  bool useType = false;
-  TheoryId typeTheoryId = THEORY_LAST;
-
-  if (current != parent) {
-    if (currentTheoryId != parentTheoryId) {
-      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
-      TypeNode type = current.getType();
-      useType = true;
-      typeTheoryId = Theory::theoryOf(type);
-    } else {
-      TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
-      if (typeTheoryId != currentTheoryId) {
-        if (type.isInterpretedFinite()) {
-          useType = true;
-        }
-      }
-    }
-  }
   
   // Get the theories that have already visited this node
   TNodeToTheorySetMap::iterator find = d_visited.find(current);
   if (find == d_visited.end()) {
-    if (useType) {
-      d_theories = TheoryIdSetUtil::setInsert(typeTheoryId, d_theories);
-    }
+    // not visited at all, return false
     return false;
   }
 
   TheoryIdSet visitedTheories = (*find).second;
-  if (TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
-  {
-    // The current theory has already visited it, so now it depends on the parent and the type
-    if (TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
-    {
-      if (useType) {
-        TheoryId typeTheoryId2 = Theory::theoryOf(current.getType());
-        d_theories = TheoryIdSetUtil::setInsert(typeTheoryId2, d_theories);
-        return TheoryIdSetUtil::setContains(typeTheoryId2, visitedTheories);
-      } else {
-        return true;
-      }
-    } else {
-      return false;
-    }
-  } else {
-    return false;
-  }
+  return isAlreadyVisited(visitedTheories, current, parent);
 }
 
 void PreRegisterVisitor::visit(TNode current, TNode parent) {
@@ -112,74 +107,96 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     Debug("register::internal") << toString() << std::endl;
   }
 
-  // Get the theories of the terms
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
-
-  // Should we use the theory of the type
-  bool useType = false;
-  TheoryId typeTheoryId = THEORY_LAST;
-
-  if (current != parent) {
-    if (currentTheoryId != parentTheoryId) {
-      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
-      TypeNode type = current.getType();
-      useType = true;
-      typeTheoryId = Theory::theoryOf(type);
-    } else {
-      TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
-      if (typeTheoryId != currentTheoryId) {
-        if (type.isInterpretedFinite()) {
-          useType = true;
-        }
-      }
-    }
-  }
-
+  // get the theories we already preregistered with
   TheoryIdSet visitedTheories = d_visited[current];
+
+  // call the preregistration on current, parent or type theories and update
+  // visitedTheories.
+  preRegister(d_engine, visitedTheories, current, parent);
+
   Debug("register::internal")
       << "PreRegisterVisitor::visit(" << current << "," << parent
-      << "): previously registered with "
+      << "): now registered with "
       << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
-  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
+  // update the theories set for current
+  d_visited[current] = visitedTheories;
+  Assert(d_visited.find(current) != d_visited.end());
+  Assert(alreadyVisited(current, parent));
+}
+
+void PreRegisterVisitor::preRegister(TheoryEngine* te,
+                                     TheoryIdSet& visitedTheories,
+                                     TNode current,
+                                     TNode parent)
+{
+  // Preregister with the current theory, if necessary
+  TheoryId currentTheoryId = Theory::theoryOf(current);
+  preRegisterWithTheory(te, visitedTheories, currentTheoryId, current, parent);
+
+  if (current != parent)
   {
-    visitedTheories =
-        TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories);
-    d_visited[current] = visitedTheories;
-    Theory* th = d_engine->theoryOf(currentTheoryId);
-    th->preRegisterTerm(current);
-    Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
+    // preregister with parent theory, if necessary
+    TheoryId parentTheoryId = Theory::theoryOf(parent);
+    preRegisterWithTheory(te, visitedTheories, parentTheoryId, current, parent);
+
+    // Note that if enclosed by different theories it's shared, for example,
+    // in read(a, f(a)), f(a) should be shared with integers.
+    TypeNode type = current.getType();
+    if (currentTheoryId != parentTheoryId || type.isInterpretedFinite())
+    {
+      // preregister with the type's theory, if necessary
+      TheoryId typeTheoryId = Theory::theoryOf(type);
+      preRegisterWithTheory(te, visitedTheories, typeTheoryId, current, parent);
+    }
   }
-  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
+}
+void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
+                                               TheoryIdSet& visitedTheories,
+                                               TheoryId id,
+                                               TNode current,
+                                               TNode parent)
+{
+  if (TheoryIdSetUtil::setContains(id, visitedTheories))
   {
-    visitedTheories =
-        TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories);
-    d_visited[current] = visitedTheories;
-    Theory* th = d_engine->theoryOf(parentTheoryId);
-    th->preRegisterTerm(current);
-    Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
+    // already registered
+    return;
   }
-  if (useType) {
-    if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories))
+  if (Configuration::isAssertionBuild())
+  {
+    Debug("register::internal")
+        << "PreRegisterVisitor::visit(" << current << "," << parent
+        << "): adding " << id << std::endl;
+    // This should never throw an exception, since theories should be
+    // guaranteed to be initialized.
+    // These checks don't work with finite model finding, because it
+    // uses Rational constants to represent cardinality constraints,
+    // even though arithmetic isn't actually involved.
+    if (!options::finiteModelFind())
     {
-      visitedTheories =
-          TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories);
-      d_visited[current] = visitedTheories;
-      Theory* th = d_engine->theoryOf(typeTheoryId);
-      th->preRegisterTerm(current);
-      Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
+      if (!te->isTheoryEnabled(id))
+      {
+        const LogicInfo& l = te->getLogicInfo();
+        LogicInfo newLogicInfo = l.getUnlockedCopy();
+        newLogicInfo.enableTheory(id);
+        newLogicInfo.lock();
+        std::stringstream ss;
+        ss << "The logic was specified as " << l.getLogicString()
+           << ", which doesn't include " << id
+           << ", but found a term in that theory." << std::endl
+           << "You might want to extend your logic to "
+           << newLogicInfo.getLogicString() << std::endl;
+        throw LogicException(ss.str());
+      }
     }
   }
-  Debug("register::internal")
-      << "PreRegisterVisitor::visit(" << current << "," << parent
-      << "): now registered with "
-      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
-
-  Assert(d_visited.find(current) != d_visited.end());
-  Assert(alreadyVisited(current, parent));
+  // call the theory's preRegisterTerm method
+  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
+  Theory* th = te->theoryOf(id);
+  th->preRegisterTerm(current);
 }
 
+void PreRegisterVisitor::start(TNode node) {}
+
 std::string SharedTermsVisitor::toString() const {
   std::stringstream ss;
   TNodeVisitedMap::const_iterator it = d_visited.begin();
@@ -206,59 +223,14 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
     return true;
   }
   TNodeVisitedMap::const_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;
   }
 
-  TheoryIdSet theories = (*find).second;
-
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
-
-  // Should we use the theory of the type
-  bool useType = false;
-  TheoryId typeTheoryId = THEORY_LAST;
-
-  if (current != parent) {
-    if (currentTheoryId != parentTheoryId) {
-      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
-      TypeNode type = current.getType();
-      useType = true;
-      typeTheoryId = Theory::theoryOf(type);
-    } else {
-      TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
-      if (typeTheoryId != currentTheoryId) {
-        if (type.isInterpretedFinite()) {
-          useType = true;
-        }
-      }
-    }
-  }
-
-  if (TheoryIdSetUtil::setContains(currentTheoryId, theories))
-  {
-    if (TheoryIdSetUtil::setContains(parentTheoryId, theories))
-    {
-      if (useType)
-      {
-        return TheoryIdSetUtil::setContains(typeTheoryId, theories);
-      }
-      else
-      {
-        return true;
-      }
-    }
-    else
-    {
-      return false;
-    }
-  } else {
-    return false;
-  }
+  TheoryIdSet visitedTheories = (*find).second;
+  return isAlreadyVisited(visitedTheories, current, parent);
 }
 
 void SharedTermsVisitor::visit(TNode current, TNode parent) {
@@ -267,66 +239,16 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
   if (Debug.isOn("register::internal")) {
     Debug("register::internal") << toString() << std::endl;
   }
-
-  // Get the theories of the terms
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
-
-  // Should we use the theory of the type
-  bool useType = false;
-  TheoryId typeTheoryId = THEORY_LAST;
-
-  if (current != parent) {
-    if (currentTheoryId != parentTheoryId) {
-      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
-      TypeNode type = current.getType();
-      useType = true;
-      typeTheoryId = Theory::theoryOf(type);
-    } else {
-      TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
-      if (typeTheoryId != currentTheoryId) {
-        if (type.isInterpretedFinite()) {
-          useType = true;
-        }
-      }
-    }
-  }
-
   TheoryIdSet visitedTheories = d_visited[current];
-  Debug("register::internal")
-      << "SharedTermsVisitor::visit(" << current << "," << parent
-      << "): previously registered with "
-      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
-  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
-  {
-    visitedTheories =
-        TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories);
-    Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
-  }
-  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
-  {
-    visitedTheories =
-        TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories);
-    Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
-  }
-  if (useType) {
-    if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories))
-    {
-      visitedTheories =
-          TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories);
-      Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
-    }
-  }
-  Debug("register::internal")
-      << "SharedTermsVisitor::visit(" << current << "," << parent
-      << "): now registered with "
-      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
+
+  // preregister the term with the current, parent or type theories, as needed
+  PreRegisterVisitor::preRegister(d_engine, visitedTheories, current, parent);
 
   // Record the new theories that we visited
   d_visited[current] = visitedTheories;
 
   // If there is more than two theories and a new one has been added notify the shared terms database
+  TheoryId currentTheoryId = Theory::theoryOf(current);
   if (TheoryIdSetUtil::setDifference(
           visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
   {
@@ -338,7 +260,7 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
 }
 
 void SharedTermsVisitor::start(TNode node) {
-  clear();
+  d_visited.clear();
   d_atom = node;
 }
 
@@ -350,3 +272,5 @@ void SharedTermsVisitor::clear() {
   d_atom = TNode();
   d_visited.clear();
 }
+
+}  // namespace CVC4