diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-21 16:47:57 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-21 16:47:57 -0800 |
| commit | 9f7e50702810aafd0ce67a79b4c5906b48aec4b4 (patch) | |
| tree | 171a8b232f4874bfa3ff52d4fae264fd24002065 /test | |
| parent | f0bc0137d00946f79e62e223b849e7372cc0109f (diff) | |
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 42ac2cdd9..8139f1c2e 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -221,6 +221,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node a = d_nm->mkConst(::CVC4::String("A")); Node b = d_nm->mkConst(::CVC4::String("B")); Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); + Node negone = d_nm->mkConst(Rational(-1)); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); Node two = d_nm->mkConst(Rational(2)); @@ -330,6 +331,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node substr_itos = d_nm->mkNode( kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x); sameNormalForm(substr_itos, empty); + + // (str.substr s (* (- 1) (str.len s)) 1) ---> empty + Node substr = d_nm->mkNode( + kind::STRING_SUBSTR, + s, + d_nm->mkNode(kind::MULT, negone, d_nm->mkNode(kind::STRING_LENGTH, s)), + one); + sameNormalForm(substr, empty); } void testRewriteConcat() |