diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-29 10:10:59 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-29 10:10:59 -0800 |
commit | 94b509bfc6e12848bdbb924bd53e6e11900b1989 (patch) | |
tree | d3df5f5a6a2bb8f878e6ad42369afd9eb1f2c563 | |
parent | 0334a62d2b6d54055fcfee6d182439a5b056d44d (diff) | |
parent | 030cdf1e7f61034dda5b9ed8fd4925d87c6a1c3d (diff) |
Merge branch 'fixStripConstantEndpoints' into cav2019strings
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 6 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 17 |
2 files changed, 23 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b0ad90c29..90bd91070 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -3584,6 +3584,12 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, unsigned index1 = r == 0 ? 0 : n2.size() - 1; bool removeComponent = false; Node n1cmp = n1[index0]; + + if (n1cmp.isConst() && n1cmp.getConst<String>().size() == 0) + { + return false; + } + std::vector<Node> sss; std::vector<Node> sls; n1cmp = decomposeSubstrChain(n1cmp, sss, sls); diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index e699fd40c..f98ac233b 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1184,6 +1184,23 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } } + void testStripConstantEndpoints() + { + Node empty = d_nm->mkConst(::CVC4::String("")); + Node a = d_nm->mkConst(::CVC4::String("A")); + + { + // stripConstantEndpoints({ "" }, { "a" }, {}, {}, 0) ---> false + std::vector<Node> n1 = {empty}; + std::vector<Node> n2 = {a}; + std::vector<Node> nb; + std::vector<Node> ne; + bool res = + TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + TS_ASSERT(!res); + } + } + private: ExprManager* d_em; SmtEngine* d_smt; |