Strengthen contains rewrites

2 files changed, 102 insertions, 14 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8e5e22d38..349a8b4fb 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2017,13 +2017,6 @@ 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)
   {
@@ -2068,14 +2061,25 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   }
   else if (node[0].getKind() == kind::STRING_SUBSTR)
   {
-    // (str.contains (str.substr x n (str.len y)) y) --->
-    //   (= (str.substr x n (str.len y)) y)
-    //
-    // TODO: Remove with under-/over-approximation
-    if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
+    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)
     {
-      Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
-      return returnRewrite(node, ret, "ctn-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)
@@ -2150,6 +2154,18 @@ 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;
 }
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 59d36d9e8..760e35471 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -448,6 +448,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node negOne = d_nm->mkConst(Rational(-1));
+    Node zero = d_nm->mkConst(Rational(0));
     Node one = d_nm->mkConst(Rational(1));
     Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
@@ -486,6 +487,32 @@ 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);
+    }
+
+    // (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,
+              d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one),
+              b),
+          a,
+          zero);
+      sameNormalForm(idof, negOne);
+    }
   }
 
   void testRewriteReplace()
@@ -634,6 +661,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node aac = d_nm->mkConst(::CVC4::String("AAC"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
     Node x = d_nm->mkVar("x", strType);
@@ -642,6 +670,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
     Node z = d_nm->mkVar("z", strType);
     Node n = d_nm->mkVar("n", intType);
+    Node m = d_nm->mkVar("m", intType);
+    Node zero = d_nm->mkConst(Rational(0));
     Node one = d_nm->mkConst(Rational(1));
     Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
@@ -874,6 +904,48 @@ 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()