diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 3c40062f5..befe52574 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2948,6 +2948,13 @@ Node SequencesRewriter::rewriteReplaceRe(Node node) return returnRewrite(node, x, Rewrite::REPLACE_RE_EVAL); } } + // str.replace_re( x, y, z ) ---> z ++ x if "" in y ---> true + String emptyStr(""); + if (RegExpEntail::testConstStringInRegExp(emptyStr, 0, y)) + { + Node ret = nm->mkNode(STRING_CONCAT, z, x); + return returnRewrite(node, ret, Rewrite::REPLACE_RE_EMP_RE); + } return node; } |