Strip non-matching beginning from indexof operator (#2885)

This commit adds a rewrite that strips endpoints from `str.indexof`
operators if they don't overlap with the string that is being searched
for using `stripConstantEndpoints()`. In addition to that, it makes
`stripConstantEndpoints()` slightly more aggressive by allowing it to
drop substring components that have zero overlap with the string that we
are looking at. Finally, the commit fixes the default argument for
`fullRewriter` of `checkEntailContains()` to be true instead of false,
which should allow for more rewriting opportunities.

1 files changed, 70 insertions, 0 deletions

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 881941568..4650bbf27 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -445,13 +445,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
     Node aaad = d_nm->mkConst(::CVC4::String("AAAD"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node c = d_nm->mkConst(::CVC4::String("C"));
+    Node ccc = d_nm->mkConst(::CVC4::String("CCC"));
     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));
     Node i = d_nm->mkVar("i", intType);
+    Node j = d_nm->mkVar("j", intType);
 
     // Same normal form for:
     //
@@ -486,6 +490,54 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                      a,
                      i);
     sameNormalForm(idof_substr, negOne);
+
+    {
+      // Same normal form for:
+      //
+      // (str.indexof (str.++ "B" (str.substr "CCC" i j) x "A") "A" 0)
+      //
+      // (+ 1 (str.len (str.substr "CCC" i j))
+      //    (str.indexof (str.++ "A" x y) "A" 0))
+      Node lhs = d_nm->mkNode(
+          kind::STRING_STRIDOF,
+          d_nm->mkNode(kind::STRING_CONCAT,
+                       b,
+                       d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j),
+                       x,
+                       a),
+          a,
+          zero);
+      Node rhs = d_nm->mkNode(
+          kind::PLUS,
+          one,
+          d_nm->mkNode(kind::STRING_LENGTH,
+                       d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j)),
+          d_nm->mkNode(kind::STRING_STRIDOF,
+                       d_nm->mkNode(kind::STRING_CONCAT, x, a),
+                       a,
+                       zero));
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // Same normal form for:
+      //
+      // (str.indexof (str.++ "B" "C" "A" x y) "A" 0)
+      //
+      // (+ 2 (str.indexof (str.++ "A" x y) "A" 0))
+      Node lhs = d_nm->mkNode(kind::STRING_STRIDOF,
+                              d_nm->mkNode(kind::STRING_CONCAT, b, c, a, x, y),
+                              a,
+                              zero);
+      Node rhs =
+          d_nm->mkNode(kind::PLUS,
+                       two,
+                       d_nm->mkNode(kind::STRING_STRIDOF,
+                                    d_nm->mkNode(kind::STRING_CONCAT, a, x, y),
+                                    a,
+                                    zero));
+      sameNormalForm(lhs, rhs);
+    }
   }
 
   void testRewriteReplace()
@@ -648,6 +700,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node ab = d_nm->mkConst(::CVC4::String("AB"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
     Node abc = d_nm->mkConst(::CVC4::String("ABC"));
@@ -659,6 +712,7 @@ 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 one = d_nm->mkConst(Rational(1));
     Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
@@ -930,6 +984,22 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
       rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc);
       differentNormalForms(lhs, rhs);
     }
+
+    {
+      // Same normal form for:
+      //
+      // (str.contains (str.++ (str.substr "DEF" n m) x) "AB")
+      //
+      // (str.contains x "AB")
+      lhs = d_nm->mkNode(
+          kind::STRING_STRCTN,
+          d_nm->mkNode(kind::STRING_CONCAT,
+                       d_nm->mkNode(kind::STRING_SUBSTR, def, n, m),
+                       x),
+          ab);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ab);
+      sameNormalForm(lhs, rhs);
+    }
   }
 
   void testInferEqsFromContains()