From dbe3d6da12fc30eb3bdf00d640e7457fba67e8dc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Sep 2018 18:35:54 -0500 Subject: [PATCH] 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. --- src/theory/strings/theory_strings_rewriter.cpp | 16 +--------------- 1 file changed, 1 insertion(+), 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