diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-24 00:11:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-24 05:11:24 +0000 |
| commit | 7179be03b049d3046140316c4c5987efbdbd09b8 (patch) | |
| tree | 194f889c2b8cb6c02fcd244818add0c365de96d9 /src/theory/quantifiers | |
| parent | 421803a044faf8f17ebf6d44f94adbdfdbded4a6 (diff) | |
Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)
There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 40e28eb78..f5883c265 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1710,7 +1710,8 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret) const if (ret.getKind() == EQUAL) { - new_ret = strings::SequencesRewriter(nullptr).rewriteEqualityExt(ret); + strings::SequencesRewriter sr(&d_rew, nullptr); + new_ret = sr.rewriteEqualityExt(ret); } return new_ret; |