diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-21 17:44:50 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-21 17:44:50 -0800 |
| commit | eb7226ebeabf7cc70ec023107d74ffc5c1bad5e7 (patch) | |
| tree | 5cc95c4afb046f4c38e7bcd2c682cd2790634d04 /src/theory/quantifiers/extended_rewrite.cpp | |
| parent | 9f7e50702810aafd0ce67a79b4c5906b48aec4b4 (diff) | |
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.cpp')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 404bb850c..b583a55da 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1676,6 +1676,10 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret) { new_ret = strings::TheoryStringsRewriter::rewriteEqualityExt(ret); } + else if (ret.getKind() == STRING_SUBSTR) + { + new_ret = strings::TheoryStringsRewriter::rewriteSubstrExt(ret); + } return new_ret; } |