From b80720f15170b02cbc93a53095ec2dd96bb8029c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 22 Mar 2019 03:48:56 +0000
Subject: [PATCH] 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.
---
 .../strings/theory_strings_rewriter.cpp       | 12 +--
 .../theory/theory_strings_rewriter_white.h    | 76 +++++++++++++++++++
 2 files changed, 82 insertions(+), 6 deletions(-)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 79667b9aa..0763fa7d5 100644
--- 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 79a50d533..881941568 100644
--- 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()
-- 
2.30.2