diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 11:44:29 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-26 13:44:29 -0500 |
commit | 2126fcefd7bf593e949a7a5a71b1d56878f710db (patch) | |
tree | 71a5217392db11dcf63a38227784e260575c5de0 /test/unit/theory | |
parent | 6bdc464d5f2e2dac39230dfef8da1049e0b317d1 (diff) |
Add reasoning for inequalities in str rewriter (#1713)
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 50 |
1 files changed, 46 insertions, 4 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index a1e878f6e..a17299f80 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -72,27 +72,53 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node x_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero)); - // x + (str.len y) = 0 /\ 0 >= x --> true + // x + (str.len y) = 0 |= 0 >= x --> true TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( x_plus_slen_y_eq_zero, zero, x, false)); - // x + (str.len y) = 0 /\ 0 > x --> false + // x + (str.len y) = 0 |= 0 > x --> false TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( x_plus_slen_y_eq_zero, zero, x, true)); Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode( kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); - // x + (str.len y) + z = 0 /\ 0 > x --> false + // x + (str.len y) + z = 0 |= 0 > x --> false TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( x_plus_slen_y_plus_z_eq_zero, zero, x, true)); Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode( kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero)); - // x + (str.len y) + (str.len y) = 0 /\ 0 >= x --> true + // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); + + Node five = d_nm->mkConst(Rational(5)); + Node six = d_nm->mkConst(Rational(6)); + Node x_plus_five = d_nm->mkNode(kind::PLUS, x, five); + Node x_plus_five_lt_six = + Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six)); + + // x + 5 < 6 |= 0 >= x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_five_lt_six, zero, x, false)); + + // x + 5 < 6 |= 0 > x --> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_five_lt_six, zero, x, true)); + + Node neg_x = d_nm->mkNode(kind::UMINUS, x); + Node x_plus_five_lt_five = + Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, five)); + + // x + 5 < 5 |= -x >= 0 --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_five_lt_five, neg_x, zero, false)); + + // x + 5 < 5 |= 0 > x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_five_lt_five, zero, x, false)); } void testRewriteSubstr() @@ -102,6 +128,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node empty = d_nm->mkConst(::CVC4::String("")); Node a = d_nm->mkConst(::CVC4::String("A")); + Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); + Node two = d_nm->mkConst(Rational(2)); + Node three = d_nm->mkConst(Rational(3)); + Node s = d_nm->mkVar("s", strType); Node x = d_nm->mkVar("x", intType); Node y = d_nm->mkVar("y", intType); @@ -132,5 +162,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y); res = TheoryStringsRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); + + // (str.substr "ABCD" (+ x 3) x) -> "" + n = d_nm->mkNode( + kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) + n = d_nm->mkNode( + kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, n); } }; |