diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-03 10:05:01 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-03 12:05:01 -0600 |
| commit | d47530bd5924286781325cf2db3477e83a3c6d4f (patch) | |
| tree | 25c709632df6029b6bccd94b22d7f21662c8adf8 /test | |
| parent | 8a114b1899a5b31dfe733b0dd4ed897942e43f03 (diff) | |
Rewrite `str.contains` used for character matching (#3519)
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index c5db12c6c..b5eb92900 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -703,9 +703,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node ab = d_nm->mkConst(::CVC4::String("AB")); Node b = d_nm->mkConst(::CVC4::String("B")); Node c = d_nm->mkConst(::CVC4::String("C")); + Node e = d_nm->mkConst(::CVC4::String("E")); + Node h = d_nm->mkConst(::CVC4::String("H")); + Node j = d_nm->mkConst(::CVC4::String("J")); + Node p = d_nm->mkConst(::CVC4::String("P")); 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 abbchijp = d_nm->mkConst(::CVC4::String("ABBCHIJP")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); @@ -1000,6 +1005,37 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ab); sameNormalForm(lhs, rhs); } + + { + // Same normal form for: + // + // (str.contains "ABBCHIJP" (str.at x n)) + // + // (or (= x "") + // (and (<= (str.code "A") (str.code (str.at x n))) + // (<= (str.code (str.at x n)) (str.code "C"))) + // (and (<= (str.code "H") (str.code (str.at x n))) + // (<= (str.code (str.at x n)) (str.code "J"))) + // (= (str.code (str.at x n)) (str.code "P"))) + Node cat = d_nm->mkNode(kind::STRING_CHARAT, x, n); + lhs = d_nm->mkNode(kind::STRING_STRCTN, abbchijp, cat); + Node ca = d_nm->mkNode(kind::STRING_CODE, a); + Node cc = d_nm->mkNode(kind::STRING_CODE, c); + Node ch = d_nm->mkNode(kind::STRING_CODE, h); + Node cj = d_nm->mkNode(kind::STRING_CODE, j); + Node cp = d_nm->mkNode(kind::STRING_CODE, p); + Node ccat = d_nm->mkNode(kind::STRING_CODE, cat); + rhs = d_nm->mkNode(kind::OR, + d_nm->mkNode(kind::EQUAL, cat, empty), + d_nm->mkNode(kind::AND, + d_nm->mkNode(kind::LEQ, ca, ccat), + d_nm->mkNode(kind::LEQ, ccat, cc)), + d_nm->mkNode(kind::AND, + d_nm->mkNode(kind::LEQ, ch, ccat), + d_nm->mkNode(kind::LEQ, ccat, cj)), + d_nm->mkNode(kind::EQUAL, ccat, cp)); + sameNormalForm(lhs, rhs); + } } void testInferEqsFromContains() |