diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:06:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-12 18:06:27 -0700 |
commit | 470bff2ea4b964f08a93c551f3f8722f66c738ad (patch) | |
tree | 6a69ac4d89d976ea552e6e6786c4cc8a2cf9291d /test | |
parent | 3f960e4f3744121efddd19b12806fee660887497 (diff) | |
parent | 8597f207187baff3b9f8cc5d8955e5b96d6d57d0 (diff) |
Merge branch 'master' into subsolverParamssubsolverParams
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() |