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/sets | |
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/sets')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 5 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 12 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 |
4 files changed, 8 insertions, 14 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 63ebacc23..0bf2ed2ea 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -98,9 +98,10 @@ void TheorySets::check(Effort e) { d_internal->check(e); } -bool TheorySets::collectModelInfo(TheoryModel* m) +bool TheorySets::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { - return d_internal->collectModelInfo(m); + return d_internal->collectModelValues(m, termSet); } void TheorySets::computeCareGraph() { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a7fb31dab..a826a43af 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -60,7 +60,8 @@ class TheorySets : public Theory void notifySharedTerm(TNode) override; void check(Effort) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; void computeCareGraph() override; TrustNode explain(TNode) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3c9414606..78824636a 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1258,18 +1258,10 @@ std::string traceElements(const Node& set) } // namespace -bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) +bool TheorySetsPrivate::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { Trace("sets-model") << "Set collect model info" << std::endl; - set<Node> termSet; - // Compute terms appearing in assertions and shared terms - d_external.computeRelevantTerms(termSet); - - // Assert equalities and disequalities to the model - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - return false; - } NodeManager* nm = NodeManager::currentNM(); std::map<Node, Node> mvals; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index af780eadc..387d56de9 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -176,7 +176,7 @@ class TheorySetsPrivate { void check(Theory::Effort); - bool collectModelInfo(TheoryModel* m); + bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet); void computeCareGraph(); |