Make stripConstantEndpoints() less aggressive

`stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)`
was cutting off "A" because it is a non-digit. This is wrong, however,
because `(int.to.str n)` can return the empty string. This commit
makes `stripConstantEndpoints()` less aggressive by not using
`str.to.int` terms to cut off non-digits anymore.

2 files changed, 28 insertions, 21 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8d9d6a230..cbb298c5f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3683,26 +3683,6 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
             overlap = s.size() - ret;
           }
         }
-        else if (n2[index1].getKind() == kind::STRING_ITOS)
-        {
-          const std::vector<unsigned>& svec = s.getVec();
-          // can remove up to the first occurrence of a digit
-          unsigned svsize = svec.size();
-          for (unsigned i = 0; i < svsize; i++)
-          {
-            unsigned sindex = r == 0 ? i : (svsize - 1) - i;
-            if (String::isDigit(svec[sindex]))
-            {
-              break;
-            }
-            else if (sss.empty())  // only if not substr
-            {
-              // e.g. str.contains( str.++( "a", x ), int.to.str(y) ) -->
-              // str.contains( x, int.to.str(y) )
-              overlap--;
-            }
-          }
-        }
         else
         {
           // inconclusive
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 6eb022eea..5b4846a12 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1224,15 +1224,30 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
           d_nm->mkNode(kind::STRING_CONCAT, x, b));
       sameNormalForm(eq, f);
     }
+
+    {
+      // (= (str.++ "A" (int.to.str n)) "A") -/-> false
+      Node eq = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, a, d_nm->mkNode(kind::STRING_ITOS, n)), a);
+      differentNormalForms(eq, f);
+    }
   }
 
   void testStripConstantEndpoints()
   {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node ab = d_nm->mkConst(::CVC4::String("AB"));
+    Node cd = d_nm->mkConst(::CVC4::String("CD"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node n = d_nm->mkVar("n", intType);
 
     {
-      // stripConstantEndpoints({ "" }, { "a" }, {}, {}, 0) ---> false
+      // stripConstantEndpoints({ "" }, { "A" }, {}, {}, 0) ---> false
       std::vector<Node> n1 = {empty};
       std::vector<Node> n2 = {a};
       std::vector<Node> nb;
@@ -1241,6 +1256,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
           TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
       TS_ASSERT(!res);
     }
+
+    {
+      // stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)
+      // ---> false
+      std::vector<Node> n1 = {a};
+      std::vector<Node> n2 = {a, d_nm->mkNode(kind::STRING_ITOS, n)};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
+      TS_ASSERT(!res);
+    }
   }
 
   void testRewriteMembership()