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, 52 insertions, 23 deletions

diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 94fc83b30..6e09d90cc 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -51,21 +51,16 @@ class PreRegisterVisitor {
   TNodeToTheorySetMap d_visited;
 
   /**
-   * A set of all theories in the term
-   */
-  theory::TheoryIdSet d_theories;
-
-  /**
    * String representation of the visited map, for debugging purposes.
    */
   std::string toString() const;
 
  public:
-  /** Returned set tells us which theories there are */
-  typedef theory::TheoryIdSet return_type;
+  /** required to instantiate template for NodeVisitor */
+  using return_type = void;
 
   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
-      : d_engine(engine), d_visited(context), d_theories(0)
+      : d_engine(engine), d_visited(context)
   {
   }
 
@@ -82,14 +77,43 @@ class PreRegisterVisitor {
   void visit(TNode current, TNode parent);
 
   /**
-   * Marks the node as the starting literal.
+   * Marks the node as the starting literal, which does nothing. This method
+   * is required to instantiate template for NodeVisitor.
    */
-  void start(TNode node) {}
+  void start(TNode node);
+
+  /** Called when the visitor is finished with a term, do nothing */
+  void done(TNode node) {}
 
   /**
-   * Notifies the engine of all the theories used.
+   * Preregister the term current occuring under term parent.  This calls
+   * Theory::preRegisterTerm for the theories of current and parent, as well
+   * as the theory of current's type, if it is finite.
+   *
+   * This method takes a set of theories visitedTheories that have already
+   * preregistered current and updates this set with the theories that
+   * preregister current during this call
+   *
+   * @param te Pointer to the theory engine containing the theories
+   * @param visitedTheories The theories that have already preregistered current
+   * @param current The term to preregister
+   * @param parent The parent term of current
    */
-  theory::TheoryIdSet done(TNode node) { return d_theories; }
+  static void preRegister(TheoryEngine* te,
+                          theory::TheoryIdSet& visitedTheories,
+                          TNode current,
+                          TNode parent);
+
+ private:
+  /**
+   * Helper for above, called whether we wish to register a term with a theory
+   * given by an identifier id.
+   */
+  static void preRegisterWithTheory(TheoryEngine* te,
+                                    theory::TheoryIdSet& visitedTheories,
+                                    theory::TheoryId id,
+                                    TNode current,
+                                    TNode parent);
 };
 
 
@@ -100,9 +124,6 @@ class PreRegisterVisitor {
  */
 class SharedTermsVisitor {
 
-  /** The shared terms database */
-  SharedTermsDatabase& d_sharedTerms;
-
   /**
    * Cache from preprocessing of atoms.
    */
@@ -118,14 +139,16 @@ class SharedTermsVisitor {
   /** 
    * The initial atom.
    */
-  TNode d_atom; 
-    
-public:
+  TNode d_atom;
 
-  typedef void return_type;
+ public:
+  /** required to instantiate template for NodeVisitor */
+  using return_type = void;
 
-  SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
-  : d_sharedTerms(sharedTerms) {}
+  SharedTermsVisitor(TheoryEngine* te, SharedTermsDatabase& sharedTerms)
+      : d_engine(te), d_sharedTerms(sharedTerms)
+  {
+  }
 
   /**
    * Returns true is current has already been pre-registered with both current and parent theories.
@@ -136,9 +159,9 @@ public:
    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
    */
   void visit(TNode current, TNode parent);
-  
+
   /**
-   * Marks the node as the starting literal.
+   * Marks the node as the starting literal, which clears the state.
    */
   void start(TNode node);
 
@@ -151,6 +174,12 @@ public:
    * Clears the internal state.
    */   
   void clear();
+
+ private:
+  /** The engine */
+  TheoryEngine* d_engine;
+  /** The shared terms database */
+  SharedTermsDatabase& d_sharedTerms;
 };