diff options
| -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++ ){ |