move collectAssertedTerms back to the theory class (#7018)

This PR moves the collectAssertedTerms utility function from the model manager to the theory class. This allows to use the utility also when we are not currently building the model.

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 0d56dd6dbf2ad391bd7e26e5a64efbc2b520faf6..9d25dd76043663cd23aa5c9fcf4fa8e3183fc1f6 100644 (file)
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -175,63 +175,5 @@ 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())
-    {
-      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 cvc5

diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index ff8459fcb9a61b14d4ad0a947d2c35cad0624418..fd8ca6e11462a5d615993bf7fbb2ac17c8159cf0 100644 (file)
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -108,22 +108,7 @@ 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;
   /** Reference to the environment */

diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 4124407bee70552cdba85e8baa8b22567da80d67..91e4cb6d4a7de7ddbdbdf972e3629078ba7204f1 100644 (file)
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -81,11 +81,19 @@ bool ModelManagerDistributed::prepareModel()
       continue;
     }
     Theory* t = d_te.theoryOf(theoryId);
+    if (theoryId == TheoryId::THEORY_BOOL
+        || theoryId == TheoryId::THEORY_BUILTIN)
+    {
+      Trace("model-builder")
+          << "  Skipping theory " << theoryId
+          << " as it does not contribute to the model anyway" << std::endl;
+      continue;
+    }
     Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
                            << std::endl;
     // collect the asserted terms
     std::set<Node> termSet;
-    collectAssertedTerms(theoryId, termSet);
+    t->collectAssertedTerms(termSet);
     // also get relevant terms
     t->computeRelevantTerms(termSet);
     if (!t->collectModelInfo(d_model.get(), termSet))

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 04bab16e22155a5790e13298dd40b952eb662412..5ca1979b3f029eaa866b02f1e97035cbaa9ef5e8 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -387,6 +387,60 @@ void Theory::computeRelevantTerms(std::set<Node>& termSet)
   // by default, there are no additional relevant terms
 }
 
+void Theory::collectAssertedTerms(std::set<Node>& termSet,
+                                  bool includeShared) const
+{
+  // Collect all terms appearing in assertions
+  context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
+                                             assert_it_end = facts_end();
+  for (; assert_it != assert_it_end; ++assert_it)
+  {
+    collectTerms(*assert_it, termSet);
+  }
+
+  if (includeShared)
+  {
+    // Add terms that are shared terms
+    context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
+                                           shared_it_end = shared_terms_end();
+    for (; shared_it != shared_it_end; ++shared_it)
+    {
+      collectTerms(*shared_it, termSet);
+    }
+  }
+}
+
+void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
+{
+  const std::set<Kind>& irrKinds =
+      d_theoryState->getModel()->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())
+    {
+      termSet.insert(cur);
+    }
+    // traverse owned terms, don't go under quantifiers
+    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id)
+        && !cur.isClosure())
+    {
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+}
+
 bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
   return true;

diff --git a/src/theory/theory.h b/src/theory/theory.h
index a857931a896ef22bf5559aa845420c11246cb7e5..7c76c7ee67e17f3ab312bac5943f921b47693c29 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -638,6 +638,19 @@ class Theory {
    * shared terms that should be considered relevant, add them to termSet.
    */
   virtual void computeRelevantTerms(std::set<Node>& termSet);
+  /**
+   * Collect asserted terms for this theory and add them to  termSet.
+   *
+   * @param termSet The set to add terms to
+   * @param includeShared Whether to include the shared terms of the theory
+   */
+  void collectAssertedTerms(std::set<Node>& termSet,
+                            bool includeShared = true) const;
+  /**
+   * Helper function for collectAssertedTerms, adds all subterms
+   * belonging to this theory to termSet.
+   */
+  void collectTerms(TNode n, std::set<Node>& termSet) const;
   /**
    * Collect model values, after equality information is added to the model.
    * The argument termSet is the set of relevant terms returned by