Standardization of Theory (#5181)

This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 5ea2799c5..7d121af53 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -78,7 +78,12 @@ bool ModelManagerDistributed::prepareModel()
     Theory* t = d_te.theoryOf(theoryId);
     Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
                            << std::endl;
-    if (!t->collectModelInfo(d_model))
+    // collect the asserted terms
+    std::set<Node> termSet;
+    collectAssertedTerms(theoryId, termSet);
+    // also get relevant terms
+    t->computeRelevantTerms(termSet);
+    if (!t->collectModelInfo(d_model, termSet))
     {
       Trace("model-builder")
           << "ModelManagerDistributed: fail collect model info" << std::endl;