diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-03 16:17:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-02-03 16:17:37 -0800 |
| commit | b396d78982e109dc642611d32578bbca82b210cd (patch) | |
| tree | e29dce4fdd0c2190860ddbc9f1c611f9eb443a83 /test/unit | |
| parent | e374c7fbde3b3a5148b6e8fc302277b6e786965e (diff) | |
Add rewrite for contains + const strings replace (#2828)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index bbaa4733f..191d0ba58 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -650,6 +650,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node a = d_nm->mkConst(::CVC4::String("A")); Node b = d_nm->mkConst(::CVC4::String("B")); Node c = d_nm->mkConst(::CVC4::String("C")); + Node abc = d_nm->mkConst(::CVC4::String("ABC")); + Node def = d_nm->mkConst(::CVC4::String("DEF")); + Node ghi = d_nm->mkConst(::CVC4::String("GHI")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); @@ -888,6 +891,45 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite d_nm->mkNode(kind::STRING_CONCAT, b, x)); sameNormalForm(ctn, f); } + + { + // Same normal form for: + // + // (str.contains (str.replace x "ABC" "DEF") "GHI") + // + // (str.contains x "GHI") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), + ghi); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ghi); + sameNormalForm(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "ABC" "DEF") "B") + // + // (str.contains x "B") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), + b); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b); + differentNormalForms(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "B" "DEF") "ABC") + // + // (str.contains x "ABC") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, b, def), + abc); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } } void testInferEqsFromContains() |