Make stripConstantEndpoints() less aggressive (#2830)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e8abc37a543f630bcb1ee2d30f4e9276e66f42fc..eff68ebe6bd88f183fdfe396d302f490b0045452 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3647,26 +3647,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 191d0ba580f141b2f6f55aa5b7565e45182b3f21..c5d20daefcc6272090f55f1e84b12fe303510f2f 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1220,15 +1220,33 @@ 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;
@@ -1237,6 +1255,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);
+    }
   }
 
  private: