diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 19:27:31 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-26 21:27:31 -0500 |
commit | 6a656809c353776c9de9580b19a6de79ef5a76d4 (patch) | |
tree | 74a8c90517ec1711dcc4faa65c0620ffe298b9de /test/unit | |
parent | ab70f7a01939515792221b33372ec994bd425fde (diff) |
Better normalization of string concatenation (#1719)
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index a17299f80..acee9754b 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -175,4 +175,74 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite res = TheoryStringsRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); } + + void testRewriteConcat() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node empty = d_nm->mkConst(::CVC4::String("")); + Node a = d_nm->mkConst(::CVC4::String("A")); + Node zero = d_nm->mkConst(Rational(0)); + Node three = d_nm->mkConst(Rational(3)); + + Node i = d_nm->mkVar("i", intType); + Node s = d_nm->mkVar("s", strType); + Node x = d_nm->mkVar("x", strType); + Node y = d_nm->mkVar("y", strType); + + // Same normal form for: + // + // (str.++ (str.replace "A" x "") "A") + // + // (str.++ "A" (str.replace "A" x "")) + Node repl_a_x_e = d_nm->mkNode(kind::STRING_STRREPL, a, x, empty); + Node repl_a = d_nm->mkNode(kind::STRING_CONCAT, repl_a_x_e, a); + Node a_repl = d_nm->mkNode(kind::STRING_CONCAT, a, repl_a_x_e); + Node res_repl_a = Rewriter::rewrite(repl_a); + Node res_a_repl = Rewriter::rewrite(a_repl); + TS_ASSERT_EQUALS(res_repl_a, res_a_repl); + + // Same normal form for: + // + // (str.++ y (str.replace "" x (str.substr y 0 3)) (str.substr y 0 3) "A" (str.substr y 0 3)) + // + // (str.++ y (str.substr y 0 3) (str.replace "" x (str.substr y 0 3)) "A" (str.substr y 0 3)) + Node z = d_nm->mkNode(kind::STRING_SUBSTR, y, zero, three); + Node repl_e_x_z = d_nm->mkNode(kind::STRING_STRREPL, empty, x, z); + repl_a = d_nm->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z); + a_repl = d_nm->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z); + res_repl_a = Rewriter::rewrite(repl_a); + res_a_repl = Rewriter::rewrite(a_repl); + TS_ASSERT_EQUALS(res_repl_a, res_a_repl); + + // Same normal form for: + // + // (str.++ "A" (str.replace "A" x "") (str.substr "A" 0 i)) + // + // (str.++ (str.substr "A" 0 i) (str.replace "A" x "") "A") + Node substr_a = d_nm->mkNode(kind::STRING_SUBSTR, a, zero, i); + Node a_substr_repl = + d_nm->mkNode(kind::STRING_CONCAT, a, substr_a, repl_a_x_e); + Node substr_repl_a = + d_nm->mkNode(kind::STRING_CONCAT, substr_a, repl_a_x_e, a); + Node res_a_substr_repl = Rewriter::rewrite(a_substr_repl); + Node res_substr_repl_a = Rewriter::rewrite(substr_repl_a); + TS_ASSERT_EQUALS(res_a_substr_repl, res_substr_repl_a); + + // Same normal form for: + // + // (str.++ (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i) (str.at "A" i)) + // + // (str.++ (str.at "A" i) (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i)) + Node charat_a = d_nm->mkNode(kind::STRING_CHARAT, a, i); + Node repl_e_x_s = d_nm->mkNode(kind::STRING_STRREPL, empty, x, substr_a); + Node repl_substr_a = + d_nm->mkNode(kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a); + Node a_repl_substr = + d_nm->mkNode(kind::STRING_CONCAT, charat_a, repl_e_x_s, substr_a); + Node res_repl_substr_a = Rewriter::rewrite(repl_substr_a); + Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr); + TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr); + } }; |