diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 13:19:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 13:19:18 -0500 |
commit | ec24a92382d0884e5b9b07a8c2f2ed056c98ae9a (patch) | |
tree | faa0e082ae46491c9f01a91e980309b88978a252 /src | |
parent | 8fd4ac8bff4aa7a4b4e04e35f6944d303d5cf498 (diff) |
Add string rewrite involving allchar stars (#3167)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 70 |
1 files changed, 54 insertions, 16 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index aac2477ea..32190e093 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -763,7 +763,12 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) Trace("strings-rewrite-debug") << "Strings::rewriteConcatRegExp start " << node << std::endl; std::vector<Node> cvec; + // the current accumulation of constant strings std::vector<Node> preReStr; + // whether the last component was (_)* + bool lastAllStar = false; + String emptyStr = String(""); + // this loop checks to see if components can be combined or dropped for (unsigned i = 0, size = vec.size(); i <= size; i++) { Node curr; @@ -771,42 +776,58 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) { curr = vec[i]; Assert(curr.getKind() != REGEXP_CONCAT); - if (!cvec.empty() && preReStr.empty()) - { - Node cvecLast = cvec.back(); - if (cvecLast.getKind() == REGEXP_STAR && cvecLast[0] == curr) - { - // by convention, flip the order (a*)++a ---> a++(a*) - cvec[cvec.size() - 1] = curr; - cvec.push_back(cvecLast); - curr = Node::null(); - } - } } // update preReStr if (!curr.isNull() && curr.getKind() == STRING_TO_REGEXP) { + lastAllStar = false; preReStr.push_back(curr[0]); curr = Node::null(); } else if (!preReStr.empty()) { + Assert(!lastAllStar); // this groups consecutive strings a++b ---> ab Node acc = nm->mkNode(STRING_TO_REGEXP, utils::mkConcat(STRING_CONCAT, preReStr)); cvec.push_back(acc); preReStr.clear(); } - if (!curr.isNull() && curr.getKind() == REGEXP_STAR) + else if (!curr.isNull() && lastAllStar) { - // we can group stars (a*)++(a*) ---> a* - if (!cvec.empty() && cvec.back() == curr) + // if empty, drop it + // e.g. this ensures we rewrite (_)* ++ (a)* ---> (_)* + if (testConstStringInRegExp(emptyStr, 0, curr)) { curr = Node::null(); } } if (!curr.isNull()) { + lastAllStar = false; + if (curr.getKind() == REGEXP_STAR) + { + // we can group stars (a)* ++ (a)* ---> (a)* + if (!cvec.empty() && cvec.back() == curr) + { + curr = Node::null(); + } + else if (curr[0].getKind() == REGEXP_SIGMA) + { + Assert(!lastAllStar); + lastAllStar = true; + // go back and remove empty ones from back of cvec + // e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)* + while (!cvec.empty() + && testConstStringInRegExp(emptyStr, 0, cvec.back())) + { + cvec.pop_back(); + } + } + } + } + if (!curr.isNull()) + { cvec.push_back(curr); } } @@ -814,10 +835,27 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) retNode = utils::mkConcat(REGEXP_CONCAT, cvec); if (retNode != node) { - // handles all cases where consecutive re constants are combined, and cases - // where arguments are swapped, as described in the loop above. + // handles all cases where consecutive re constants are combined or dropped + // as described in the loop above. return returnRewrite(node, retNode, "re.concat"); } + + // flipping adjacent star arguments + changed = false; + for (size_t i = 0, size = cvec.size() - 1; i < size; i++) + { + if (cvec[i].getKind() == REGEXP_STAR && cvec[i][0] == cvec[i + 1]) + { + // by convention, flip the order (a*)++a ---> a++(a*) + std::swap(cvec[i], cvec[i+1]); + changed = true; + } + } + if (changed) + { + retNode = utils::mkConcat(REGEXP_CONCAT, cvec); + return returnRewrite(node, retNode, "re.concat.opt"); + } return node; } |