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

1 files changed, 59 insertions, 0 deletions

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