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 | |
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.
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 9 |
3 files changed, 28 insertions, 6 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; } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 57a99532e..0de42f686 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1806,8 +1806,18 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } } } + Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; + return node; +} + +Node TheoryStringsRewriter::rewriteSubstrExt(Node node) +{ + Assert(node.getKind() == STRING_SUBSTR); + + NodeManager* nm = NodeManager::currentNM(); + // combine substr - if (node[0].getKind() == kind::STRING_SUBSTR) + if (node[0].getKind() == STRING_SUBSTR) { Node start_inner = node[0][1]; Node start_outer = node[1]; @@ -1820,7 +1830,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) // the length of a string from the inner substr subtracts the start point // of the outer substr Node len_from_inner = - Rewriter::rewrite(nm->mkNode(kind::MINUS, node[0][2], start_outer)); + Rewriter::rewrite(nm->mkNode(MINUS, node[0][2], start_outer)); Node len_from_outer = node[2]; Node new_len; // take quantity that is for sure smaller than the other @@ -1838,14 +1848,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } if (!new_len.isNull()) { - Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer); - Node ret = - nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len); + Node new_start = nm->mkNode(PLUS, start_inner, start_outer); + Node ret = nm->mkNode(STRING_SUBSTR, node[0][0], new_start, new_len); return returnRewrite(node, ret, "ss-combine"); } } } - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; + return node; } diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 69d6ff68e..7731cd078 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -159,12 +159,21 @@ class TheoryStringsRewriter { * Returns the rewritten form of node. */ static Node rewriteConcat(Node node); + /** rewrite substr * This is the entry point for post-rewriting terms node of the form * str.substr( s, i1, i2 ) * Returns the rewritten form of node. */ static Node rewriteSubstr(Node node); + + /** rewrite substr extended + * This is the entry point for extended post-rewriting terms node of the form + * str.substr( s, i1, i2 ) + * Returns the rewritten form of node. + */ + static Node rewriteSubstrExt(Node node); + /** rewrite contains * This is the entry point for post-rewriting terms node of the form * str.contains( t, s ) |