Add irrelevant kinds infrastructure to TheoryModel (#4945)

Currently, Theory is responsible for implementing a computeRelevantTerms method collects the union of:
(1) The terms appearing in its assertions and its shared terms,
(2) The set of additional terms the theory believes are relevant.

Currently, (1) is computed by an internal Theory method computeRelevantTermsInternal, and the overall computeRelevantTerms is overridden by the theory (for datatypes and arrays only) for also including (2).

The new plan is that Theory will only need to compute (2). Computing (1) will be the job of ModelManager::collectAssertedTerms and the model manager will call Theory::computeRelevantTerms as an additional step prior to its calls to collect model info.

This will make certain optimizations possible in theory combination (e.g. tracking asserted terms incrementally).

This PR adds the ModelManager::collectAssertedTerms method and also adds infrastructure for irrelevant kinds in the model object (which have an analogous interface as when "unevaluated" kinds are marked during initialization). It does not connect the implementation yet.

FYI @barrettcw

7 files changed, 117 insertions, 0 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f85b79c53..c7e2c7c1b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -108,6 +108,8 @@ void TheoryDatatypes::finishInit()
     // do congruence on evaluation functions
     d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
   }
+  // testers are not relevant for model building
+  d_valuation.setIrrelevantKind(APPLY_TESTER);
 }
 
 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 1451b6ab0..89daa922c 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -162,5 +162,64 @@ bool ModelManager::collectModelBooleanVariables()
   return true;
 }
 
+void ModelManager::collectAssertedTerms(TheoryId tid,
+                                        std::set<Node>& termSet,
+                                        bool includeShared) const
+{
+  Theory* t = d_te.theoryOf(tid);
+  // Collect all terms appearing in assertions
+  context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(),
+                                             assert_it_end = t->facts_end();
+  for (; assert_it != assert_it_end; ++assert_it)
+  {
+    collectTerms(tid, *assert_it, termSet);
+  }
+
+  if (includeShared)
+  {
+    // Add terms that are shared terms
+    context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(),
+                                           shared_it_end =
+                                               t->shared_terms_end();
+    for (; shared_it != shared_it_end; ++shared_it)
+    {
+      collectTerms(tid, *shared_it, termSet);
+    }
+  }
+}
+
+void ModelManager::collectTerms(TheoryId tid,
+                                TNode n,
+                                std::set<Node>& termSet) const
+{
+  const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds();
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (termSet.find(cur) != termSet.end())
+    {
+      // already visited
+      continue;
+    }
+    Kind k = cur.getKind();
+    // only add to term set if a relevant kind
+    if (irrKinds.find(k) == irrKinds.end())
+    {
+      Assert(Theory::theoryOf(cur) == tid);
+      termSet.insert(cur);
+    }
+    // traverse owned terms, don't go under quantifiers
+    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid)
+        && !cur.isClosure())
+    {
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 12b99dc18..9fc2e1156 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -91,6 +91,22 @@ class ModelManager
    * @return true if we are in conflict.
    */
   bool collectModelBooleanVariables();
+  /**
+   * Collect asserted terms for theory with the given identifier, add to
+   * termSet.
+   *
+   * @param tid The theory whose assertions we are collecting
+   * @param termSet The set to add terms to
+   * @param includeShared Whether to include the shared terms of the theory
+   */
+  void collectAssertedTerms(TheoryId tid,
+                            std::set<Node>& termSet,
+                            bool includeShared = true) const;
+  /**
+   * Helper function for collectAssertedTerms, adds all subterms
+   * belonging to theory tid to termSet.
+   */
+  void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
   /** Reference to the theory engine */
   TheoryEngine& d_te;
   /** Logic info of theory engine (cached) */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 31b44aa70..869e9100e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -72,6 +72,12 @@ void TheoryModel::finishInit()
   {
     setSemiEvaluatedKind(kind::APPLY_UF);
   }
+  // Equal and not terms are not relevant terms. In other words, asserted
+  // equalities and negations of predicates (as terms) do not need to be sent
+  // to the model. Regardless, theories should send information to the model
+  // that ensures that all assertions are satisfied.
+  setIrrelevantKind(EQUAL);
+  setIrrelevantKind(NOT);
 }
 
 void TheoryModel::reset(){
@@ -627,6 +633,13 @@ void TheoryModel::setSemiEvaluatedKind(Kind k)
   d_semi_evaluated_kinds.insert(k);
 }
 
+void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); }
+
+const std::set<Kind>& TheoryModel::getIrrelevantKinds() const
+{
+  return d_irrKinds;
+}
+
 bool TheoryModel::isLegalElimination(TNode x, TNode val)
 {
   return !expr::hasSubtermKinds(d_unevaluated_kinds, val);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index b725cfa09..c31f208a0 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -262,6 +262,17 @@ public:
    */
   void setUnevaluatedKind(Kind k);
   void setSemiEvaluatedKind(Kind k);
+  /**
+   * Set irrelevant kind. These kinds do not impact model generation, that is,
+   * registered terms in theories of this kind do not need to be sent to
+   * the model. An example is APPLY_TESTER.
+   */
+  void setIrrelevantKind(Kind k);
+  /**
+   * Get the set of irrelevant kinds that have been registered by the above
+   * method.
+   */
+  const std::set<Kind>& getIrrelevantKinds() const;
   /** is legal elimination
    *
    * Returns true if x -> val is a legal elimination of variable x.
@@ -358,6 +369,8 @@ public:
   std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
   /** a set of kinds that are semi-evaluated */
   std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
+  /** The set of irrelevant kinds */
+  std::set<Kind> d_irrKinds;
   /**
    * Map of representatives of equality engine to used representatives in
    * representative set
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 9375a4868..bec528215 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -145,6 +145,15 @@ void Valuation::setSemiEvaluatedKind(Kind k)
   }
 }
 
+void Valuation::setIrrelevantKind(Kind k)
+{
+  TheoryModel* m = getModel();
+  if (m != nullptr)
+  {
+    m->setIrrelevantKind(k);
+  }
+}
+
 Node Valuation::ensureLiteral(TNode n) {
   Assert(d_engine != nullptr);
   return d_engine->ensureLiteral(n);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 35d990715..dc12d030d 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -122,6 +122,11 @@ public:
    * See TheoryModel::setSemiEvaluatedKind for details.
    */
   void setSemiEvaluatedKind(Kind k);
+  /**
+   * Set that k is an irrelevant kind in the TheoryModel, if it exists.
+   * See TheoryModel::setIrrelevantKind for details.
+   */
+  void setIrrelevantKind(Kind k);
   //-------------------------------------- end static configuration of the model
 
   /**