diff options
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 76 |
1 files changed, 76 insertions, 0 deletions
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() |