diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-11 15:00:26 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-11 17:00:26 -0500 |
| commit | 4338b1fc7e14e98bcbb651e6fddafd1154ae1f2b (patch) | |
| tree | c1e38828ec5843751f20f0c7704dcad51d729eb0 /test | |
| parent | 82ddf4c77bf234d08feaa884d9ead245abcead81 (diff) | |
Improve reasoning about empty strings in rewriter (#2615)
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index d967ab793..cc29efb23 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -381,6 +381,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); Node z = d_nm->mkVar("z", strType); + Node zero = d_nm->mkConst(Rational(0)); + Node one = d_nm->mkConst(Rational(1)); // (str.replace (str.replace x "B" x) x "A") --> // (str.replace (str.replace x "B" "A") x "A") @@ -452,6 +454,32 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite d_nm->mkNode(kind::STRING_STRREPL, y, x, a), y); sameNormalForm(repl_repl, empty); + + // (str.replace "" (str.replace x y x) x) ---> "" + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + empty, + d_nm->mkNode(kind::STRING_STRREPL, x, y, x), + x); + sameNormalForm(repl_repl, empty); + + // (str.replace "" (str.substr x 0 1) x) ---> "" + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + empty, + d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one), + x); + sameNormalForm(repl_repl, empty); + + // Same normal form for: + // + // (str.replace "" (str.replace x y x) y) + // + // (str.replace "" x y) + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + empty, + d_nm->mkNode(kind::STRING_STRREPL, x, y, x), + y); + Node repl = d_nm->mkNode(kind::STRING_STRREPL, empty, x, y); + sameNormalForm(repl_repl, repl); } void testRewriteContains() |