From fbf6733b9c182d0e0ecedfaa5dc9f576f6f1607f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 18 Aug 2021 16:20:30 -0700 Subject: [PATCH] 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. --- src/theory/model_manager.cpp | 58 ------------------------ src/theory/model_manager.h | 17 +------ src/theory/model_manager_distributed.cpp | 10 +++- src/theory/theory.cpp | 54 ++++++++++++++++++++++ src/theory/theory.h | 13 ++++++ 5 files changed, 77 insertions(+), 75 deletions(-) diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 0d56dd6db..9d25dd760 100644 --- 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& termSet, - bool includeShared) const -{ - Theory* t = d_te.theoryOf(tid); - // Collect all terms appearing in assertions - context::CDList::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::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& termSet) const -{ - const std::set& irrKinds = d_model->getIrrelevantKinds(); - std::vector 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 ff8459fcb..fd8ca6e11 100644 --- 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& 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& 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 4124407be..91e4cb6d4 100644 --- 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 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 04bab16e2..5ca1979b3 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -387,6 +387,60 @@ void Theory::computeRelevantTerms(std::set& termSet) // by default, there are no additional relevant terms } +void Theory::collectAssertedTerms(std::set& termSet, + bool includeShared) const +{ + // Collect all terms appearing in assertions + context::CDList::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::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& termSet) const +{ + const std::set& irrKinds = + d_theoryState->getModel()->getIrrelevantKinds(); + std::vector 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& termSet) { return true; diff --git a/src/theory/theory.h b/src/theory/theory.h index a857931a8..7c76c7ee6 100644 --- 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& 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& termSet, + bool includeShared = true) const; + /** + * Helper function for collectAssertedTerms, adds all subterms + * belonging to this theory to termSet. + */ + void collectTerms(TNode n, std::set& termSet) const; /** * Collect model values, after equality information is added to the model. * The argument termSet is the set of relevant terms returned by -- 2.30.2