diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-20 07:20:12 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-20 09:20:12 -0500 |
| commit | f3e1b280ae2bcea29856b9a113633e7064a08faa (patch) | |
| tree | ec42e3da1ce7d790ece4e1e1df6e35f65c782041 /test | |
| parent | 1d4324bf87a35e36d9cc1e856d74ffbaf912a848 (diff) | |
Add substr, contains and equality rewrites (#2665)
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 87817872b..87aef3704 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -145,6 +145,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node z = d_nm->mkVar("z", intType); Node zero = d_nm->mkConst(Rational(0)); + Node one = d_nm->mkConst(Rational(1)); + + Node empty = d_nm->mkConst(::CVC4::String("")); + Node a = d_nm->mkConst(::CVC4::String("A")); Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y); Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y); @@ -198,6 +202,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite // x + 5 < 5 |= 0 > x --> true TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( x_plus_five_lt_five, zero, x, false)); + + // 0 < x |= x >= (str.len (int.to.str x)) + Node assm = Rewriter::rewrite(d_nm->mkNode(kind::LT, zero, x)); + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + assm, + x, + d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)), + false)); } void testRewriteSubstr() @@ -313,6 +325,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite substr_y, b); sameNormalForm(substr_repl, repl_substr); + + // (str.substr (str.int.to.str x) x x) ---> empty + Node substr_itos = d_nm->mkNode( + kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x); + sameNormalForm(substr_itos, empty); } void testRewriteConcat() @@ -816,6 +833,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite rhs = d_nm->mkNode( kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, z, y), y); sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x "A" "B") "A") + // + // (str.contains (str.replace x "A" "") "A") + lhs = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), a); + rhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, a, empty), + a); + sameNormalForm(lhs, rhs); } void testInferEqsFromContains() @@ -1024,6 +1053,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), empty); Node eq_x = d_nm->mkNode(kind::EQUAL, x, empty); sameNormalForm(eq_repl, eq_x); + + // Same normal form for: + // + // (= (str.replace y "A" "B") "B") + // + // (= (str.replace y "B" "A") "A") + Node lhs = d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b); + Node rhs = d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a); + sameNormalForm(lhs, rhs); } private: |