summaryrefslogtreecommitdiff
path: root/src/theory/sets/theory_sets.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-31 14:24:27 -0500
committerGitHub <noreply@github.com>2020-08-31 12:24:27 -0700
commit7b3b19f73ceb2168ced48d07a590c0f3be82a8d4 (patch)
treea2ca8f1cae261c87ea659c2d8f36a8090475e88d /src/theory/sets/theory_sets.h
parent57a02fd0c7faa7a87b8619d52cf519e033633c1d (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/theory_sets.h')
-rw-r--r--src/theory/sets/theory_sets.h3
1 files changed, 2 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback