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/arith | |
| 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/arith')
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 8ca99d369..9a8ca733a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4140,8 +4140,8 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; std::set<Node> termSet; - d_containing.computeRelevantTerms(termSet); - + const std::set<Kind>& irrKinds = m->getIrrelevantKinds(); + d_containing.computeAssertedTerms(termSet, irrKinds, true); // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); |