Simplify interface for computing relevant terms. (#4966)

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

16 files changed, 73 insertions, 100 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 8ca99d369..9a8ca733a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4140,8 +4140,8 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
   std::set<Node> termSet;
-  d_containing.computeRelevantTerms(termSet);
- 
+  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
+  d_containing.computeAssertedTerms(termSet, irrKinds, true);
 
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b4a234748..3adcd4f49 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1090,19 +1090,11 @@ void TheoryArrays::computeCareGraph()
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-bool TheoryArrays::collectModelInfo(TheoryModel* m)
+bool TheoryArrays::collectModelValues(TheoryModel* m,
+                                      const std::set<Node>& termSet)
 {
-  // Compute terms appearing in assertions and shared terms, and also
-  // include additional reads due to the RIntro1 and RIntro2 rules.
-  std::set<Node> termSet;
-  computeRelevantTerms(termSet);
-
-  // Send the equality engine information to the model
-  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
-  {
-    return false;
-  }
-
+  // termSet contains terms appearing in assertions and shared terms, and also
+  // includes additional reads due to the RIntro1 and RIntro2 rules.
   NodeManager* nm = NodeManager::currentNM();
   // Compute arrays that we need to produce representatives for
   std::vector<Node> arrays;
@@ -2263,13 +2255,8 @@ TrustNode TheoryArrays::expandDefinition(Node node)
   return TrustNode::null();
 }
 
-void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet,
-                                        bool includeShared)
+void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet)
 {
-  // include all standard terms
-  std::set<Kind> irrKinds;
-  computeRelevantTermsInternal(termSet, irrKinds, includeShared);
-
   NodeManager* nm = NodeManager::currentNM();
   // make sure RIntro1 reads are included in the relevant set of reads
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8cbf826c1..9044b9950 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -264,7 +264,8 @@ class TheoryArrays : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
  public:
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS
@@ -480,11 +481,10 @@ class TheoryArrays : public Theory {
   Node getNextDecisionRequest();
 
   /**
-   * Compute relevant terms. This includes additional select nodes for the
+   * Compute relevant terms. This includes select nodes for the
    * RIntro1 and RIntro2 rules.
    */
-  void computeRelevantTerms(std::set<Node>& termSet,
-                            bool includeShared = true) override;
+  void computeRelevantTerms(std::set<Node>& termSet) override;
 };/* class TheoryArrays */
 
 }/* CVC4::theory::arrays namespace */
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index c3a305952..83e286f10 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -540,7 +540,8 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
 bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
 {
   std::set<Node> termSet;
-  d_bv->computeRelevantTerms(termSet);
+  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
+  d_bv->computeAssertedTerms(termSet, irrKinds, true);
 
   for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
     TNode var = *it;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e5a416a1b..80a6aeb86 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -715,7 +715,8 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
   AlwaysAssert(!d_quickSolver->inConflict());
   set<Node> termSet;
-  d_bv->computeRelevantTerms(termSet);
+  const std::set<Kind>& irrKinds = model->getIrrelevantKinds();
+  d_bv->computeAssertedTerms(termSet, irrKinds, true);
 
   // collect relevant terms that the bv theory abstracts to variables
   // (variables and parametric terms such as select apply_uf)
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d8f376a74..38c5cb482 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -354,7 +354,8 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
     }
   }
   set<Node> termSet;
-  d_bv->computeRelevantTerms(termSet);
+  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
+  d_bv->computeAssertedTerms(termSet, irrKinds, true);
   if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
     return false;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a98c77a5d..4c8fa87ba 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1483,7 +1483,8 @@ void TheoryDatatypes::computeCareGraph(){
   Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
 }
 
-bool TheoryDatatypes::collectModelInfo(TheoryModel* m)
+bool TheoryDatatypes::collectModelValues(TheoryModel* m,
+                                         const std::set<Node>& termSet)
 {
   Trace("dt-cmi") << "Datatypes : Collect model info "
                   << d_equalityEngine->consistent() << std::endl;
@@ -1491,17 +1492,6 @@ bool TheoryDatatypes::collectModelInfo(TheoryModel* m)
   printModelDebug( "dt-model" );
   Trace("dt-model") << std::endl;
 
-  std::set<Node> termSet;
-
-  // Compute terms appearing in assertions and shared terms, and in inferred equalities
-  computeRelevantTerms(termSet);
-
-  //combine the equality engine
-  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
-  {
-    return false;
-  }
-
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator(d_equalityEngine);
   std::vector< Node > cons;
@@ -2218,15 +2208,8 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
   }
 }
 
-void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet,
-                                           bool includeShared)
+void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet)
 {
-  // Compute terms appearing in assertions and shared terms
-  std::set<Kind> irrKinds;
-  // testers are not relevant for model construction
-  irrKinds.insert(APPLY_TESTER);
-  computeRelevantTermsInternal(termSet, irrKinds, includeShared);
-
   Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..."
                   << std::endl;
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 0d5df098d..211653125 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -288,7 +288,8 @@ private:
   TrustNode ppRewrite(TNode n) override;
   void notifySharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   void shutdown() override {}
   std::string identify() const override
   {
@@ -347,11 +348,10 @@ private:
   TNode getRepresentative( TNode a );
 
   /**
-   * Compute relevant terms. In addition to all terms in assertions and shared
-   * terms, this includes datatypes in non-singleton equivalence classes.
+   * Compute relevant terms. This includes datatypes in non-singleton
+   * equivalence classes.
    */
-  void computeRelevantTerms(std::set<Node>& termSet,
-                            bool includeShared = true) override;
+  void computeRelevantTerms(std::set<Node>& termSet) override;
 
   /** sygus symmetry breaking utility */
   std::unique_ptr<SygusExtension> d_sygusExtension;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 4c59b1c06..5eb9e576d 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -1023,7 +1023,8 @@ bool TheoryFp::collectModelInfo(TheoryModel* m)
 {
   std::set<Node> relevantTerms;
   // Work out which variables are needed
-  computeRelevantTerms(relevantTerms);
+  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/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();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0de0cc33c..846f9240d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -260,7 +260,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
   std::set<Node> termSet;
 
   // Compute terms appearing in assertions and shared terms
-  computeRelevantTerms(termSet);
+  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
+  computeAssertedTerms(termSet, irrKinds);
   // assert the (relevant) portion of the equality engine to the model
   if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 66541a63e..d69c6edc5 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -359,8 +359,15 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
 
 bool Theory::collectModelInfo(TheoryModel* m)
 {
+  // NOTE: the computation of termSet will be moved to model manager
+  // and passed as an argument to collectModelInfo.
   std::set<Node> termSet;
   // Compute terms appearing in assertions and shared terms
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  const std::set<Kind>& irrKinds = tm->getIrrelevantKinds();
+  computeAssertedTerms(termSet, irrKinds, true);
+  // Compute additional relevant terms (theory-specific)
   computeRelevantTerms(termSet);
   // if we are using an equality engine, assert it to the model
   if (d_equalityEngine != nullptr)
@@ -375,7 +382,7 @@ bool Theory::collectModelInfo(TheoryModel* m)
 }
 
 void Theory::collectTerms(TNode n,
-                          set<Kind>& irrKinds,
+                          const std::set<Kind>& irrKinds,
                           set<Node>& termSet) const
 {
   if (termSet.find(n) != termSet.end()) {
@@ -396,13 +403,11 @@ void Theory::collectTerms(TNode n,
   }
 }
 
-void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
-                                          std::set<Kind>& irrKinds,
-                                          bool includeShared) const
+void Theory::computeAssertedTerms(std::set<Node>& termSet,
+                                  const std::set<Kind>& irrKinds,
+                                  bool includeShared) const
 {
   // Collect all terms appearing in assertions
-  irrKinds.insert(kind::EQUAL);
-  irrKinds.insert(kind::NOT);
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
                                              assert_it_end = facts_end();
   for (; assert_it != assert_it_end; ++assert_it)
@@ -424,10 +429,9 @@ void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
   }
 }
 
-void Theory::computeRelevantTerms(std::set<Node>& termSet, bool includeShared)
+void Theory::computeRelevantTerms(std::set<Node>& termSet)
 {
-  std::set<Kind> irrKinds;
-  computeRelevantTermsInternal(termSet, irrKinds, includeShared);
+  // by default, there are no additional relevant terms
 }
 
 bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c5fcf362c..039fdebf1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -183,26 +183,10 @@ class Theory {
 
   //---------------------------------- private 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
-   * termSet.  This is used by collectModelInfo to delimit the set of
-   * terms that should be used when constructing a model.
-   *
-   * irrKinds: The kinds of terms that appear in assertions that should *not*
-   * be included in termSet. Note that the kinds EQUAL and NOT are always
-   * treated as irrelevant kinds.
-   *
-   * includeShared: Whether to include shared terms in termSet. Notice that
-   * shared terms are not influenced by irrKinds.
-   */
-  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,
+                    const std::set<Kind>& irrKinds,
                     std::set<Node>& termSet) const;
   //---------------------------------- end private collect model info
 
@@ -688,13 +672,29 @@ class Theory {
    */
   virtual bool collectModelInfo(TheoryModel* m);
   /**
-   * 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.
+   * Scans the current set of assertions and shared terms top-down
+   * until a theory-leaf is reached, and adds all terms found to
+   * termSet.  This is used by collectModelInfo to delimit the set of
+   * terms that should be used when constructing a model.
+   *
+   * @param irrKinds The kinds of terms that appear in assertions that should *not*
+   * be included in termSet. Note that the kinds EQUAL and NOT are always
+   * treated as irrelevant kinds.
+   *
+   * @param includeShared Whether to include shared terms in termSet. Notice that
+   * shared terms are not influenced by irrKinds.
+   *
+   * TODO (project #39): this method will be deleted. The version in
+   * model manager will be used.
+   */
+  void computeAssertedTerms(std::set<Node>& termSet,
+                            const std::set<Kind>& irrKinds,
+                            bool includeShared = true) const;
+  /**
+   * Compute terms that are not necessarily part of the assertions or
+   * shared terms that should be considered relevant, add them to termSet.
    */
-  virtual void computeRelevantTerms(std::set<Node>& termSet,
-                                    bool includeShared = true);
+  virtual void computeRelevantTerms(std::set<Node>& termSet);
   /**
    * Collect model values, after equality information is added to the model.
    * The argument termSet is the set of relevant terms returned by