diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 18:35:54 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-04 16:35:54 -0700 |
commit | dbe3d6da12fc30eb3bdf00d640e7457fba67e8dc (patch) | |
tree | 273142b94ba9be3837e062c4df2ca0ff15c64eb4 /src | |
parent | dd98af783ca7236acca3ee5d5bbcd0bf1df7828a (diff) |
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 354115850..e6f3da03a 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -919,8 +919,6 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { bool allSigma = true; bool allSigmaStrict = true; unsigned allSigmaMinSize = 0; - bool allString = true; - std::vector< Node > cc; for (const Node& rc : r) { Assert(rc.getKind() != kind::REGEXP_EMPTY); @@ -935,14 +933,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { else { allSigma = false; - } - if (rc.getKind() != kind::STRING_TO_REGEXP) - { - allString = false; - } - else - { - cc.push_back(rc); + break; } } if (allSigma) @@ -952,11 +943,6 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); return returnRewrite(node, retNode, "re-concat-pure-allchar"); } - else if (allString) - { - retNode = x.eqNode(mkConcat(STRING_CONCAT, cc)); - return returnRewrite(node, retNode, "re-concat-pure-str"); - } }else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){ std::vector< Node > mvec; for( unsigned i=0; i<r.getNumChildren(); i++ ){ |