diff options
| -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() |