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, 11 insertions, 7 deletions

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index 46009e23c..43117d994 100644
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -58,16 +58,18 @@ class SharedSolver
   virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0;
   //------------------------------------- end initialization
   /**
-   * Called when the given term t is pre-registered in TheoryEngine.
+   * Called when the given atom is pre-registered in TheoryEngine.
    *
-   * This adds t as an equality to propagate in the shared terms database
-   * if it is an equality, or adds its shared terms if it involves multiple
-   * theories.
+   * This calls Theory::preRegisterTerm on all subterms of atom for the
+   * appropriate theories.
    *
-   * @param t The term to preregister
-   * @param multipleTheories Whether multiple theories are present in t.
+   * Also, if sharing is enabled, this adds atom as an equality to propagate in
+   * the shared terms database if it is an equality, and adds its shared terms
+   * to the appropariate theories.
+   *
+   * @param atom The atom to preregister
    */
-  void preRegisterShared(TNode t, bool multipleTheories);
+  void preRegister(TNode atom);
   /**
    * Pre-notify assertion fact with the given atom. This is called when any
    * fact is asserted in TheoryEngine, just before it is dispatched to the
@@ -124,6 +126,8 @@ class SharedSolver
   const LogicInfo& d_logicInfo;
   /** The database of shared terms.*/
   SharedTermsDatabase d_sharedTerms;
+  /** Default visitor for pre-registration */
+  PreRegisterVisitor d_preRegistrationVisitor;
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
 };