diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-31 14:24:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-31 12:24:27 -0700 |
| commit | 7b3b19f73ceb2168ced48d07a590c0f3be82a8d4 (patch) | |
| tree | a2ca8f1cae261c87ea659c2d8f36a8090475e88d /src/theory/theory.cpp | |
| parent | 57a02fd0c7faa7a87b8619d52cf519e033633c1d (diff) | |
Simplify interface for computing relevant terms. (#4966)
This is a followup to #4945 which simplifies the contract for computeRelevantTerms.
Diffstat (limited to 'src/theory/theory.cpp')
| -rw-r--r-- | src/theory/theory.cpp | 22 |
1 files changed, 13 insertions, 9 deletions
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) |