diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 00:21:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-12 00:21:51 -0700 |
commit | 9f5fb42580e00370ea461be5a00f8debfb59b636 (patch) | |
tree | 29e982dfcd63311aeadbcc5f33560247990e54f3 /test | |
parent | a4b0e462833f89bea6a35e0adcf103201b9ebca1 (diff) |
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 74 |
1 files changed, 73 insertions, 1 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index cc29efb23..f82140181 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -80,6 +80,24 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite TS_ASSERT_DIFFERS(res_t1, res_t2); } + void testCheckEntailArith() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node z = d_nm->mkVar("z", strType); + Node n = d_nm->mkVar("n", intType); + Node one = d_nm->mkConst(Rational(1)); + + // 1 >= (str.len (str.substr z n 1)) ---> true + Node substr_z = d_nm->mkNode(kind::STRING_LENGTH, + d_nm->mkNode(kind::STRING_SUBSTR, z, n, one)); + TS_ASSERT(TheoryStringsRewriter::checkEntailArith(one, substr_z)); + + // (str.len (str.substr z n 1)) >= 1 ---> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArith(substr_z, one)); + } + void testCheckEntailArithWithAssumption() { TypeNode intType = d_nm->integerType(); @@ -497,9 +515,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x); Node z = d_nm->mkVar("z", strType); Node n = d_nm->mkVar("n", intType); - Node one = d_nm->mkConst(Rational(2)); + Node one = d_nm->mkConst(Rational(1)); + Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); Node four = d_nm->mkConst(Rational(4)); + Node t = d_nm->mkConst(true); Node f = d_nm->mkConst(false); // Same normal form for: @@ -644,6 +664,58 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node ctn_yxxy = d_nm->mkNode(kind::STRING_STRCTN, yx, xy); Node eq_yxxy = d_nm->mkNode(kind::EQUAL, yx, xy); sameNormalForm(ctn_yxxy, eq_yxxy); + + // (str.contains (str.replace x y x) x) ---> true + ctn_repl = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), x); + sameNormalForm(ctn_repl, t); + + // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true + ctn_repl = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx), x); + sameNormalForm(ctn_repl, t); + + // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x) + // ---> true + ctn_repl = d_nm->mkNode( + kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_CONCAT, + z, + d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx)), + x); + sameNormalForm(ctn_repl, t); + + // Same normal form for: + // + // (str.contains (str.replace x y x) y) + // + // (str.contains x y) + Node lhs = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), y); + Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, y); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y x) "B") + // + // (str.contains x "B") + lhs = d_nm->mkNode( + kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), b); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y x) (str.substr z n 1)) + // + // (str.contains x (str.substr z n 1)) + Node substr_z = d_nm->mkNode(kind::STRING_SUBSTR, z, n, one); + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, y, x), + substr_z); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, substr_z); + sameNormalForm(lhs, rhs); } void testInferEqsFromContains() |