Fix stripConstantEndpoints in strings rewriter (#2883)

`TheoryStringsRewriter::stripConstantEndpoints()` returns the stripped
endpoints in the vectors `nb` and `ne`. These endpoints were not
computed correctly if string literal had to be split. For example:

```
stripConstantEndpoints({ "ABC" }, { "C" }, {}, {}, 1)
```

returned `true` and only "A" for `nb` (instead of "AB") because we
mistakenly used the amount of overlap between "ABC" and "C" (which is
one) for the length of the stripped prefix.

This commit fixes the issue and adds several unit tests.

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 79667b9aa8f92e8bfc8faee3c0379517900dfdd9..0763fa7d5a62f1840d541bdb97519de31041db58 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3613,6 +3613,8 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
 {
   Assert(nb.empty());
   Assert(ne.empty());
+
+  NodeManager* nm = NodeManager::currentNM();
   bool changed = false;
   // for ( forwards, backwards ) direction
   for (unsigned r = 0; r < 2; r++)
@@ -3693,15 +3695,13 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
             // component
             if (r == 0)
             {
-              nb.push_back(
-                  NodeManager::currentNM()->mkConst(s.prefix(overlap)));
-              n1[index0] = NodeManager::currentNM()->mkConst(s.suffix(overlap));
+              nb.push_back(nm->mkConst(s.prefix(s.size() - overlap)));
+              n1[index0] = nm->mkConst(s.suffix(overlap));
             }
             else
             {
-              ne.push_back(
-                  NodeManager::currentNM()->mkConst(s.suffix(overlap)));
-              n1[index0] = NodeManager::currentNM()->mkConst(s.prefix(overlap));
+              ne.push_back(nm->mkConst(s.suffix(s.size() - overlap)));
+              n1[index0] = nm->mkConst(s.prefix(overlap));
             }
           }
         }

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 79a50d5334ad42183399dd376714ac181b92a704..8819415686a3e4debf762b557ad32224638a9913 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1240,6 +1240,10 @@ 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 abc = d_nm->mkConst(::CVC4::String("ABC"));
+    Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node bc = d_nm->mkConst(::CVC4::String("BC"));
+    Node c = d_nm->mkConst(::CVC4::String("C"));
     Node cd = d_nm->mkConst(::CVC4::String("CD"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
@@ -1267,6 +1271,78 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
           TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
       TS_ASSERT(!res);
     }
+
+    {
+      // stripConstantEndpoints({ "ABCD" }, { "C" }, {}, {}, 1)
+      // ---> true
+      // n1 is updated to { "CD" }
+      // nb is updated to { "AB" }
+      std::vector<Node> n1 = {abcd};
+      std::vector<Node> n2 = {c};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      std::vector<Node> n1r = {cd};
+      std::vector<Node> nbr = {ab};
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1);
+      TS_ASSERT(res);
+      TS_ASSERT_EQUALS(n1, n1r);
+      TS_ASSERT_EQUALS(nb, nbr);
+    }
+
+    {
+      // stripConstantEndpoints({ "ABC", x }, { "CD" }, {}, {}, 1)
+      // ---> true
+      // n1 is updated to { "C", x }
+      // nb is updated to { "AB" }
+      std::vector<Node> n1 = {abc, x};
+      std::vector<Node> n2 = {cd};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      std::vector<Node> n1r = {c, x};
+      std::vector<Node> nbr = {ab};
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1);
+      TS_ASSERT(res);
+      TS_ASSERT_EQUALS(n1, n1r);
+      TS_ASSERT_EQUALS(nb, nbr);
+    }
+
+    {
+      // stripConstantEndpoints({ "ABC" }, { "A" }, {}, {}, -1)
+      // ---> true
+      // n1 is updated to { "A" }
+      // nb is updated to { "BC" }
+      std::vector<Node> n1 = {abc};
+      std::vector<Node> n2 = {a};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      std::vector<Node> n1r = {a};
+      std::vector<Node> ner = {bc};
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1);
+      TS_ASSERT(res);
+      TS_ASSERT_EQUALS(n1, n1r);
+      TS_ASSERT_EQUALS(ne, ner);
+    }
+
+    {
+      // stripConstantEndpoints({ x, "ABC" }, { y, "A" }, {}, {}, -1)
+      // ---> true
+      // n1 is updated to { x, "A" }
+      // nb is updated to { "BC" }
+      std::vector<Node> n1 = {x, abc};
+      std::vector<Node> n2 = {y, a};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      std::vector<Node> n1r = {x, a};
+      std::vector<Node> ner = {bc};
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1);
+      TS_ASSERT(res);
+      TS_ASSERT_EQUALS(n1, n1r);
+      TS_ASSERT_EQUALS(ne, ner);
+    }
   }
 
   void testRewriteMembership()