diff options
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() |