Revert adding rewrites

2 files changed, 7 insertions, 153 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 902b5a670..061493b96 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2018,6 +2018,13 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     return returnRewrite(node, ret, "ctn-mset-nss");
   }
 
+  if (checkEntailArith(len_n2, len_n1, false))
+  {
+    // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
+    Node ret = node[0].eqNode(node[1]);
+    return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
+  }
+
   // splitting
   if (node[0].getKind() == kind::STRING_CONCAT)
   {
@@ -2060,29 +2067,6 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       }
     }
   }
-  else if (node[0].getKind() == kind::STRING_SUBSTR)
-  {
-    Node zero = nm->mkConst(Rational(0));
-    if (node[0][1] == zero && node[0][2].getKind() == kind::STRING_STRIDOF
-        && node[0][0] == node[0][2][0] && node[0][2][1] == node[1]
-        && node[0][2][2] == zero && checkEntailNonEmpty(node[1]))
-    {
-      Node ret = nm->mkConst(false);
-      return returnRewrite(node, ret, "ctn-substr-idof");
-    }
-
-    Node substr = node[0];
-    while (substr.getKind() == kind::STRING_SUBSTR)
-    {
-      substr = substr[0];
-      Node ectn = checkEntailContains(substr, node[1]);
-      if (!ectn.isNull() && !ectn.getConst<bool>())
-      {
-        Node ret = nm->mkConst(false);
-        return returnRewrite(node, ret, "ctn-substr-nested");
-      }
-    }
-  }
   else if (node[0].getKind() == kind::STRING_STRREPL)
   {
     if (node[0][0] == node[0][2])
@@ -2155,18 +2139,6 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     }
   }
 
-  // NOTE: This rewrite should be attempted at the end because we could miss
-  // out on other rewrites. E.g. if contains(x, y) can be rewritten to false
-  // then this rewrite might instead rewrite it to an equality and we have
-  // cannot detect that the equality is false because this rewrite applies
-  // again when we check if one side of the equality contains the other.
-  if (checkEntailArith(len_n2, len_n1, false))
-  {
-    // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
-    Node ret = node[0].eqNode(node[1]);
-    return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
-  }
-
   Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
@@ -2295,39 +2267,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
           Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
           return returnRewrite(node, ret, "idof-def-ctn");
         }
-
-        if (node[1].isConst())
-        {
-          CVC4::String t = node[1].getConst<String>();
-          if (t.size() == 1)
-          {
-            size_t i = 0;
-            std::vector<Node> children0;
-            getConcat(node[0], children0);
-            for (size_t size = children0.size(); i < size; i++)
-            {
-              Node ectn = checkEntailContains(children0[i], node[1]);
-              if (ectn.isNull() || ectn.getConst<bool>())
-              {
-                break;
-              }
-            }
-            Assert(i < children0.size());
-
-            if (i > 0)
-            {
-              std::vector<Node> pfxv(children0.begin(), children0.begin() + i);
-              children0.erase(children0.begin(), children0.begin() + i);
-              Node pfx = mkConcat(STRING_CONCAT, pfxv);
-              Node nn = mkConcat(STRING_CONCAT, children0);
-              Node ret = nm->mkNode(
-                  PLUS,
-                  nm->mkNode(STRING_LENGTH, pfx),
-                  nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]));
-              return returnRewrite(node, ret, "idof-def-ctn");
-            }
-          }
-        }
       }
 
       // strip symbolic length
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index e489f1106..e699fd40c 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -487,46 +487,6 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                      a,
                      i);
     sameNormalForm(idof_substr, negOne);
-
-    Node substr_idof =
-        d_nm->mkNode(kind::STRING_SUBSTR,
-                     x,
-                     zero,
-                     d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero));
-
-    // (str.indexof (str.substr x 0 (str.indexof "A" 0)) 0) ---> -1
-    {
-      Node idof = d_nm->mkNode(kind::STRING_STRIDOF, substr_idof, a, zero);
-      sameNormalForm(idof, negOne);
-    }
-
-    Node substr_substr_idof =
-        d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one);
-
-    // (str.indexof (str.++
-    //   (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "B") 0) --->
-    // -1
-    {
-      Node idof =
-          d_nm->mkNode(kind::STRING_STRIDOF,
-                       d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, b),
-                       a,
-                       zero);
-      sameNormalForm(idof, negOne);
-    }
-
-    // (str.indexof (str.++
-    //   (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "A") 0) --->
-    // (str.len (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1))
-    {
-      Node lhs =
-          d_nm->mkNode(kind::STRING_STRIDOF,
-                       d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, a),
-                       a,
-                       zero);
-      Node rhs = d_nm->mkNode(kind::STRING_LENGTH, substr_substr_idof);
-      sameNormalForm(lhs, rhs);
-    }
   }
 
   void testRewriteReplace()
@@ -932,51 +892,6 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                               d_nm->mkNode(kind::STRING_CONCAT, b, x));
       sameNormalForm(ctn, f);
     }
-
-    {
-      // (str.contains (str.substr x 0 (str.indexof x "A" zero) "A")) ---> false
-      Node ctn = d_nm->mkNode(
-          kind::STRING_STRCTN,
-          d_nm->mkNode(kind::STRING_SUBSTR,
-                       x,
-                       zero,
-                       d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero)),
-          a);
-      sameNormalForm(ctn, f);
-    }
-
-    {
-      // (str.contains
-      //   (str.substr
-      //     (str.substr x 0 (str.indexof x "AAC" zero)) 0 n) "B") --->
-      // false
-      Node ctn = d_nm->mkNode(
-          kind::STRING_STRCTN,
-          d_nm->mkNode(kind::STRING_SUBSTR,
-                       d_nm->mkNode(kind::STRING_SUBSTR, aac, zero, m),
-                       zero,
-                       n),
-          b);
-      sameNormalForm(ctn, f);
-    }
-
-    {
-      // (str.contains
-      //   (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0 1) "A") --->
-      // false
-      Node ctn = d_nm->mkNode(
-          kind::STRING_STRCTN,
-          d_nm->mkNode(
-              kind::STRING_SUBSTR,
-              d_nm->mkNode(kind::STRING_SUBSTR,
-                           x,
-                           zero,
-                           d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero)),
-              zero,
-              one),
-          a);
-      sameNormalForm(ctn, f);
-    }
   }
 
   void testInferEqsFromContains()