diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-13 12:18:09 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-13 12:18:09 -0800 |
commit | 83cd4823d6bf8e0c8e7d82afbfac824744491762 (patch) | |
tree | d53c4bc47891c6c32d5eb1a1f911aad438b3893a /test/unit/theory | |
parent | 6eb492f636d2c950a6064389dfba297baff8e08e (diff) |
Rewrite simple regexp pattern to str.contains (#2827)
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index c5d20daef..79a50d533 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1269,6 +1269,52 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } } + void testRewriteMembership() + { + TypeNode strType = d_nm->stringType(); + + std::vector<Node> vec_empty; + Node abc = d_nm->mkConst(::CVC4::String("ABC")); + Node re_abc = d_nm->mkNode(kind::STRING_TO_REGEXP, abc); + Node x = d_nm->mkVar("x", strType); + + { + // Same normal form for: + // + // (str.in.re x (re.++ (re.* re.allchar) + // (re.* re.allchar) + // (str.to.re "ABC") + // (re.* re.allchar))) + // + // (str.contains x "ABC") + Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, + d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty)); + Node lhs = d_nm->mkNode( + kind::STRING_IN_REGEXP, + x, + d_nm->mkNode( + kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star)); + Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); + sameNormalForm(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC"))) + // + // (str.contains x "ABC") + Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, + d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty)); + Node lhs = + d_nm->mkNode(kind::STRING_IN_REGEXP, + x, + d_nm->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc)); + Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } + } + private: ExprManager* d_em; SmtEngine* d_smt; |