diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-22 03:48:56 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-22 03:48:56 +0000 |
commit | b80720f15170b02cbc93a53095ec2dd96bb8029c (patch) | |
tree | 3dc2245110cf7f9e149a59e9250bc6ff1f4b66c7 | |
parent | a20702bcbb04422ddfcda5a241fd0cc0ec32edc8 (diff) |
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.
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 12 | ||||
-rw-r--r-- | test/unit/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() |