diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index f82140181..c92597224 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -173,10 +173,12 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node b = d_nm->mkConst(::CVC4::String("B")); Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); Node zero = d_nm->mkConst(Rational(0)); + Node one = d_nm->mkConst(Rational(1)); Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); Node s = d_nm->mkVar("s", strType); + Node s2 = d_nm->mkVar("s2", strType); Node x = d_nm->mkVar("x", intType); Node y = d_nm->mkVar("y", intType); @@ -238,6 +240,42 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite s, d_nm->mkNode(kind::STRING_SUBSTR, b, x, x)); sameNormalForm(lhs, rhs); + + // Same normal form: + // + // (str.substr (str.replace s "A" "B") 0 x) + // + // (str.replace (str.substr s 0 x) "A" "B") + Node substr_repl = d_nm->mkNode(kind::STRING_SUBSTR, + d_nm->mkNode(kind::STRING_STRREPL, s, a, b), + zero, + x); + Node repl_substr = + d_nm->mkNode(kind::STRING_STRREPL, + d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x), + a, + b); + sameNormalForm(substr_repl, repl_substr); + + // Same normal form: + // + // (str.substr (str.replace s (str.substr (str.++ s2 "A") 0 1) "B") 0 x) + // + // (str.replace (str.substr s 0 x) (str.substr (str.++ s2 "A") 0 1) "B") + Node substr_y = d_nm->mkNode(kind::STRING_SUBSTR, + d_nm->mkNode(kind::STRING_CONCAT, s2, a), + zero, + one); + substr_repl = + d_nm->mkNode(kind::STRING_SUBSTR, + d_nm->mkNode(kind::STRING_STRREPL, s, substr_y, b), + zero, + x); + repl_substr = d_nm->mkNode(kind::STRING_STRREPL, + d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x), + substr_y, + b); + sameNormalForm(substr_repl, repl_substr); } void testRewriteConcat() @@ -389,6 +427,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite void testRewriteReplace() { + TypeNode intType = d_nm->integerType(); TypeNode strType = d_nm->stringType(); Node empty = d_nm->mkConst(::CVC4::String("")); @@ -401,6 +440,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node z = d_nm->mkVar("z", strType); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); + Node n = d_nm->mkVar("n", intType); // (str.replace (str.replace x "B" x) x "A") --> // (str.replace (str.replace x "B" "A") x "A") @@ -498,6 +538,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite y); Node repl = d_nm->mkNode(kind::STRING_STRREPL, empty, x, y); sameNormalForm(repl_repl, repl); + + // Same normal form: + // + // (str.replace "B" (str.replace x "A" "B") "B") + // + // (str.replace "B" x "B")) + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + b, + d_nm->mkNode(kind::STRING_STRREPL, x, a, b), + b); + repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b); + sameNormalForm(repl_repl, repl); } void testRewriteContains() @@ -716,6 +768,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite substr_z); rhs = d_nm->mkNode(kind::STRING_STRCTN, x, substr_z); sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y z) z) + // + // (str.contains (str.replace x z y) y) + lhs = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, z), z); + rhs = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, z, y), y); + sameNormalForm(lhs, rhs); } void testInferEqsFromContains() @@ -914,6 +977,16 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node eq_xxa_repl_xxa = d_nm->mkNode( kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, xxa, a, b)); sameNormalForm(eq_xxa_repl_xxa, f); + + // Same normal form for: + // + // (= (str.replace x "A" "B") "") + // + // (= x "") + Node eq_repl = d_nm->mkNode( + 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); } private: |