diff options
Diffstat (limited to 'src/theory/strings/theory_strings_rewriter.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6a8cf3e98..b2fbc94b0 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1329,6 +1329,21 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = nm->mkNode(AND, nm->mkNode(LEQ, nm->mkNode(STRING_CODE, r[0]), xcode), nm->mkNode(LEQ, xcode, nm->mkNode(STRING_CODE, r[1]))); + } + else if (r.getKind() == kind::REGEXP_LOOP) + { + Node lenb = getFixedLengthForRegexp(r[0]); + if (!lenb.isNull()) + { + retNode = nm->mkNode( + AND, + nm->mkNode(STRING_IN_REGEXP, x, nm->mkNode(REGEXP_STAR, r[0])), + nm->mkNode( + GEQ, nm->mkNode(STRING_LENGTH, x), nm->mkNode(MULT, lenb, r[1])), + nm->mkNode( + LEQ, nm->mkNode(STRING_LENGTH, x), nm->mkNode(MULT, lenb, r[2]))); + return returnRewrite(node, retNode, "re-loop-const-len-body"); + } }else if(x != node[0] || r != node[1]) { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r ); } @@ -1585,7 +1600,12 @@ bool TheoryStringsRewriter::hasEpsilonNode(TNode node) { } RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { - return RewriteResponse(REWRITE_DONE, node); + Node retNode = node; + if (node.getKind() == kind::STRING_IN_REGEXP) + { + retNode = rewriteMembership(node); + } + return RewriteResponse(REWRITE_DONE, retNode); } Node TheoryStringsRewriter::rewriteSubstr(Node node) |