From 2126fcefd7bf593e949a7a5a71b1d56878f710db Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 26 Mar 2018 11:44:29 -0700 Subject: [PATCH] Add reasoning for inequalities in str rewriter (#1713) --- .../strings/theory_strings_rewriter.cpp | 68 ++++++++++++++----- src/theory/strings/theory_strings_rewriter.h | 5 +- .../theory/theory_strings_rewriter_white.h | 50 ++++++++++++-- 3 files changed, 101 insertions(+), 22 deletions(-) diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 8f9d4c596..0777d696f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1520,15 +1520,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } } - if (tot_len == nm->mkConst(Rational(1))) + // (str.substr s x y) --> "" if x < len(s) |= 0 >= y + Node n1_lt_tot_len = + Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len)); + if (checkEntailArithWithAssumption(n1_lt_tot_len, zero, node[2], false)) { - Node n1_eq_zero = - Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[1], zero)); - if (checkEntailArithWithAssumption(n1_eq_zero, zero, node[2], false)) - { - Node ret = nm->mkConst(::CVC4::String("")); - return returnRewrite(node, ret, "ss-len-one-unsat"); - } + Node ret = nm->mkConst(::CVC4::String("")); + return returnRewrite(node, ret, "ss-start-entails-zero-len"); } } if (!curr.isNull()) @@ -3019,8 +3017,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, toVisit.push_back(currChild); } } - else if (curr.getKind() == kind::VARIABLE - && Theory::theoryOf(curr) == THEORY_ARITH) + else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH) { candVars.insert(curr); } @@ -3040,8 +3037,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, toVisit.push_back(currChild); } - if (curr.getKind() == kind::VARIABLE - && Theory::theoryOf(curr) == THEORY_ARITH + if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH && candVars.find(curr) != candVars.end()) { v = curr; @@ -3071,14 +3067,55 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumption(Node assumption, Node b, bool strict) { - // TODO: Add support for inequality assumptions. - Assert(assumption.getKind() == kind::EQUAL); Assert(Rewriter::rewrite(assumption) == assumption); NodeManager* nm = NodeManager::currentNM(); + if (!assumption.isConst() && assumption.getKind() != kind::EQUAL) + { + // We rewrite inequality assumptions from x <= y to x + (str.len s) = y + // where s is some fresh string variable. We use (str.len s) because + // (str.len s) must be non-negative for the equation to hold. + Node x, y; + if (assumption.getKind() == kind::GEQ) + { + x = assumption[0]; + y = assumption[1]; + } + else + { + // (not (>= s t)) --> (>= (t - 1) s) + Assert(assumption.getKind() == kind::NOT + && assumption[0].getKind() == kind::GEQ); + x = nm->mkNode(kind::MINUS, assumption[0][1], nm->mkConst(Rational(1))); + y = assumption[0][0]; + } + + Node s = nm->mkBoundVar("s", nm->stringType()); + Node slen = nm->mkNode(kind::STRING_LENGTH, s); + assumption = Rewriter::rewrite( + nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen))); + } + Node diff = nm->mkNode(kind::MINUS, a, b); - return checkEntailArithWithEqAssumption(assumption, diff, strict); + bool res = false; + if (assumption.isConst()) + { + bool assumptionBool = assumption.getConst(); + if (assumptionBool) + { + res = checkEntailArith(diff, strict); + } + else + { + res = true; + } + } + else + { + res = checkEntailArithWithEqAssumption(assumption, diff, strict); + } + return res; } bool TheoryStringsRewriter::checkEntailArithWithAssumptions( @@ -3090,7 +3127,6 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumptions( bool res = false; for (const auto& assumption : assumptions) { - Assert(assumption.getKind() == kind::EQUAL); Assert(Rewriter::rewrite(assumption) == assumption); if (checkEntailArithWithAssumption(assumption, a, b, strict)) diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 31ad1406a..0e4cb594a 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -376,7 +376,7 @@ private: * Checks whether assumption |= a >= b (if strict is false) or * assumption |= a > b (if strict is true). The function returns true if it * can be shown that the entailment holds and false otherwise. Assumption - * must be in rewritten form and an equality assumption. + * must be in rewritten form. Assumption may be an equality or an inequality. * * Example: * @@ -393,7 +393,8 @@ private: * Checks whether assumptions |= a >= b (if strict is false) or * assumptions |= a > b (if strict is true). The function returns true if it * can be shown that the entailment holds and false otherwise. Assumptions - * must be in rewritten form and must be equality assumptions. + * must be in rewritten form. Assumptions may be an equalities or an + * inequalities. * * Example: * 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); } }; -- 2.30.2