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 /src | |
parent | 6bdc464d5f2e2dac39230dfef8da1049e0b317d1 (diff) |
Add reasoning for inequalities in str rewriter (#1713)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 68 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 5 |
2 files changed, 55 insertions, 18 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<bool>(); + 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: * |