Simplify interface for computing relevant terms. (#4966)

This is a followup to #4945 which simplifies the contract for computeRelevantTerms.

4 files changed, 8 insertions, 14 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 63ebacc23..0bf2ed2ea 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -98,9 +98,10 @@ void TheorySets::check(Effort e) {
   d_internal->check(e);
 }
 
-bool TheorySets::collectModelInfo(TheoryModel* m)
+bool TheorySets::collectModelValues(TheoryModel* m,
+                                    const std::set<Node>& termSet)
 {
-  return d_internal->collectModelInfo(m);
+  return d_internal->collectModelValues(m, termSet);
 }
 
 void TheorySets::computeCareGraph() {
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a7fb31dab..a826a43af 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -60,7 +60,8 @@ class TheorySets : public Theory
 
   void notifySharedTerm(TNode) override;
   void check(Effort) override;
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   void computeCareGraph() override;
   TrustNode explain(TNode) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 3c9414606..78824636a 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1258,18 +1258,10 @@ std::string traceElements(const Node& set)
 
 }  // namespace
 
-bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
+bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
+                                           const std::set<Node>& termSet)
 {
   Trace("sets-model") << "Set collect model info" << std::endl;
-  set<Node> termSet;
-  // Compute terms appearing in assertions and shared terms
-  d_external.computeRelevantTerms(termSet);
-
-  // Assert equalities and disequalities to the model
-  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
-  {
-    return false;
-  }
 
   NodeManager* nm = NodeManager::currentNM();
   std::map<Node, Node> mvals;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index af780eadc..387d56de9 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -176,7 +176,7 @@ class TheorySetsPrivate {
 
   void check(Theory::Effort);
 
-  bool collectModelInfo(TheoryModel* m);
+  bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet);
 
   void computeCareGraph();