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.

2 files changed, 4 insertions, 6 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 863f9a5a6..037b083f4 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -1019,12 +1019,9 @@ Node TheoryFp::getModelValue(TNode var) {
   return d_conv.getValue(d_valuation, var);
 }
 
-bool TheoryFp::collectModelInfo(TheoryModel* m)
+bool TheoryFp::collectModelInfo(TheoryModel* m,
+                                const std::set<Node>& relevantTerms)
 {
-  std::set<Node> relevantTerms;
-  // Work out which variables are needed
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  computeAssertedTerms(relevantTerms, irrKinds);
   // this override behavior to not assert equality engine
   return collectModelValues(m, relevantTerms);
 }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 16d984011..42c009893 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -75,7 +75,8 @@ class TheoryFp : public Theory {
   //--------------------------------- end standard check
 
   Node getModelValue(TNode var) override;
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelInfo(TheoryModel* m,
+                        const std::set<Node>& relevantTerms) override;
   /** Collect model values in m based on the relevant terms given by
    * relevantTerms */
   bool collectModelValues(TheoryModel* m,