diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-19 07:18:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-19 09:18:58 -0500 |
commit | 089a60266f2658e471d204fdd737e3e0d37e105c (patch) | |
tree | dd07799cf5a1a06f184ce402fab016bf54c656e0 /test | |
parent | 94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613 (diff) |
Only apply testConstStringInRegExp to const regexp (#4120)
Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/issue4070.smt2 | 6 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 40 |
3 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0ea611435..02eb15826 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -932,6 +932,7 @@ set(regress_0_tests regress0/strings/issue3440.smt2 regress0/strings/issue3497.smt2 regress0/strings/issue3657-evalLeq.smt2 + regress0/strings/issue4070.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue4070.smt2 b/test/regress/regress0/strings/issue4070.smt2 new file mode 100644 index 000000000..2de58c4d2 --- /dev/null +++ b/test/regress/regress0/strings/issue4070.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic QF_S) +(declare-fun a () String) +(declare-fun b () String) +(assert (str.in.re a (re.++ (str.to.re b) (re.* re.allchar)))) +(check-sat) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index d71df524c..af8b24a0b 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -58,6 +58,15 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite delete d_em; } + void inNormalForm(Node t) + { + Node res_t = d_rewriter->extendedRewrite(t); + + std::cout << std::endl; + std::cout << t << " ---> " << res_t << std::endl; + TS_ASSERT_EQUALS(t, res_t); + } + void sameNormalForm(Node t1, Node t2) { Node res_t1 = d_rewriter->extendedRewrite(t1); @@ -1528,6 +1537,37 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } } + void testRewriteRegexpConcat() + { + TypeNode strType = d_nm->stringType(); + + std::vector<Node> emptyArgs; + Node x = d_nm->mkVar("x", strType); + Node y = d_nm->mkVar("y", strType); + Node allStar = d_nm->mkNode(kind::REGEXP_STAR, + d_nm->mkNode(kind::REGEXP_SIGMA, emptyArgs)); + Node xReg = d_nm->mkNode(kind::STRING_TO_REGEXP, x); + Node yReg = d_nm->mkNode(kind::STRING_TO_REGEXP, y); + + { + // In normal form: + // + // (re.++ (re.* re.allchar) (re.union (str.to.re x) (str.to.re y))) + Node n = d_nm->mkNode(kind::REGEXP_CONCAT, + allStar, + d_nm->mkNode(kind::REGEXP_UNION, xReg, yReg)); + inNormalForm(n); + } + + { + // In normal form: + // + // (re.++ (str.to.re x) (re.* re.allchar)) + Node n = d_nm->mkNode(kind::REGEXP_CONCAT, xReg, allStar); + inNormalForm(n); + } + } + private: ExprManager* d_em; SmtEngine* d_smt; |