Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)

This is work towards a configurable approach to equality engine management. This PR does not change any behavior, it only reorganizes the code.

This PR introduces the standard template for collectModelInfo, which isolates the usage of equality engine in relation to the model. In the future, theories will be encouraged to use the standard template for collectModelInfo and override collectRelevantTerms/collectModelValues only. This is to allow custom theory-independent modifications to building models (e.g. don't assert equality engine to model if we are using a centralized approach).

This PR standardizes TheoryArrays and TheoryDatatypes custom implementation of collectRelevantTerms as work towards using the standard template for collectModelInfo. Notice this required separating two portions of a loop in TheoryArrays::collectModelInfo which was doing two different things (collecting arrays and relevant terms).

1 files changed, 26 insertions, 13 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4feeac394..78c6e34cb 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -183,13 +183,7 @@ class Theory {
    */
   context::CDList<TNode> d_sharedTerms;
 
-  /**
-   * Helper function for computeRelevantTerms
-   */
-  void collectTerms(TNode n,
-                    std::set<Kind>& irrKinds,
-                    std::set<Node>& termSet) const;
-
+  //---------------------------------- collect model info
   /**
    * Scans the current set of assertions and shared terms top-down
    * until a theory-leaf is reached, and adds all terms found to
@@ -203,11 +197,30 @@ class Theory {
    * includeShared: Whether to include shared terms in termSet. Notice that
    * shared terms are not influenced by irrKinds.
    */
-  void computeRelevantTerms(std::set<Node>& termSet,
-                            std::set<Kind>& irrKinds,
-                            bool includeShared = true) const;
-  /** same as above, but with empty irrKinds */
-  void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const;
+  void computeRelevantTermsInternal(std::set<Node>& termSet,
+                                    std::set<Kind>& irrKinds,
+                                    bool includeShared = true) const;
+  /**
+   * Helper function for computeRelevantTerms
+   */
+  void collectTerms(TNode n,
+                    std::set<Kind>& irrKinds,
+                    std::set<Node>& termSet) const;
+  /**
+   * Same as above, but with empty irrKinds. This version can be overridden
+   * by the theory, e.g. by restricting or extending the set of terms returned
+   * by computeRelevantTermsInternal, which is called by default with no
+   * irrKinds.
+   */
+  virtual void computeRelevantTerms(std::set<Node>& termSet,
+                                    bool includeShared = true);
+  /**
+   * Collect model values, after equality information is added to the model.
+   * The argument termSet is the set of relevant terms returned by
+   * computeRelevantTerms.
+   */
+  virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
+  //---------------------------------- end collect model info
 
   /**
    * Construct a Theory.
@@ -619,7 +632,7 @@ class Theory {
    * This method returns true if and only if the equality engine of m is
    * consistent as a result of this call.
    */
-  virtual bool collectModelInfo(TheoryModel* m) { return true; }
+  virtual bool collectModelInfo(TheoryModel* m);
   /** if theories want to do something with model after building, do it here */
   virtual void postProcessModel( TheoryModel* m ){ }
   /**