diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 9 |
2 files changed, 24 insertions, 6 deletions
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 ) |