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.

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 354115850326d87cbd5dadbffc104c939cf7a069..e6f3da03a94c22111307a3f17fc4dc8fe3966868 100644 (file)
--- 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++ ){