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, 31 insertions, 10 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 4f0cbdb6a..02f84526f 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -343,6 +343,23 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
   return currentlyShared;
 }
 
+bool Theory::collectModelInfo(TheoryModel* m)
+{
+  std::set<Node> termSet;
+  // Compute terms appearing in assertions and shared terms
+  computeRelevantTerms(termSet);
+  // if we are using an equality engine, assert it to the model
+  if (d_equalityEngine != nullptr)
+  {
+    if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
+    {
+      return false;
+    }
+  }
+  // now, collect theory-specific value assigments
+  return collectModelValues(m, termSet);
+}
+
 void Theory::collectTerms(TNode n,
                           set<Kind>& irrKinds,
                           set<Node>& termSet) const
@@ -365,16 +382,9 @@ void Theory::collectTerms(TNode n,
   }
 }
 
-
-void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
-{
-  set<Kind> irrKinds;
-  computeRelevantTerms(termSet, irrKinds, includeShared);
-}
-
-void Theory::computeRelevantTerms(set<Node>& termSet,
-                                  set<Kind>& irrKinds,
-                                  bool includeShared) const
+void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
+                                          std::set<Kind>& irrKinds,
+                                          bool includeShared) const
 {
   // Collect all terms appearing in assertions
   irrKinds.insert(kind::EQUAL);
@@ -394,6 +404,17 @@ void Theory::computeRelevantTerms(set<Node>& termSet,
   }
 }
 
+void Theory::computeRelevantTerms(std::set<Node>& termSet, bool includeShared)
+{
+  std::set<Kind> irrKinds;
+  computeRelevantTermsInternal(termSet, irrKinds, includeShared);
+}
+
+bool Theory::collectModelValues(TheoryModel* m, std::set<Node>& termSet)
+{
+  return true;
+}
+
 Theory::PPAssertStatus Theory::ppAssert(TNode in,
                                         SubstitutionMap& outSubstitutions)
 {