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, 4 insertions, 43 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9ba97fa77..a2e608b9f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -224,7 +224,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(userContext)),
       d_relManager(nullptr),
-      d_preRegistrationVisitor(this, context),
       d_eager_model_building(false),
       d_inConflict(context, false),
       d_inSatMode(false),
@@ -292,47 +291,11 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       // should not have witness
       Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
 
-      // Pre-register the terms in the atom
-      theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
-          d_preRegistrationVisitor, preprocessed);
-      theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories);
-      // Remove the top theory, if any more that means multiple theories were
-      // involved
-      bool multipleTheories =
-          TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories);
-      if (Configuration::isAssertionBuild())
-      {
-        TheoryId i;
-        // 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())
-        {
-          while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST)
-          {
-            if (!d_logicInfo.isTheoryEnabled(i))
-            {
-              LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
-              newLogicInfo.enableTheory(i);
-              newLogicInfo.lock();
-              std::stringstream ss;
-              ss << "The logic was specified as " << d_logicInfo.getLogicString()
-                << ", which doesn't include " << i
-                << ", 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());
-            }
-          }
-        }
-      }
-
-      // pre-register with the shared solver, which also handles
-      // calling prepregister on individual theories.
+      // pre-register with the shared solver, which handles
+      // calling prepregister on individual theories, adding shared terms,
+      // and setting up equalities to propagate in the shared term database.
       Assert(d_sharedSolver != nullptr);
-      d_sharedSolver->preRegisterShared(preprocessed, multipleTheories);
+      d_sharedSolver->preRegister(preprocessed);
     }
 
     // Leaving pre-register
@@ -1307,8 +1270,6 @@ void TheoryEngine::lemma(theory::TrustNode tlemma,
   // get the node
   Node node = tlemma.getNode();
   Node lemma = tlemma.getProven();
-  Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p
-                    << std::endl;
 
   Assert(!expr::hasFreeVar(lemma));