From 9cf32b5d3f12a886779b85066d8c5997b49aefc1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Oct 2021 11:07:19 -0500 Subject: [PATCH] Avoid non-terminating check with assumptions in strings rewriter (#7503) These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression. Instead, these rewrites are now moved to the extended rewriter. --- src/theory/quantifiers/extended_rewrite.cpp | 46 ++++++++++++++++--- src/theory/quantifiers/extended_rewrite.h | 3 +- src/theory/strings/arith_entail.h | 8 ++++ src/theory/strings/sequences_rewriter.cpp | 45 +++--------------- test/regress/CMakeLists.txt | 1 + .../strings/non-terminating-rewrite-aent.smt2 | 11 +++++ test/unit/theory/sequences_rewriter_white.cpp | 11 ++--- 7 files changed, 73 insertions(+), 52 deletions(-) create mode 100644 test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index f5883c265..3d20f66b3 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -22,7 +22,9 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" +#include "theory/strings/word.h" #include "theory/theory.h" using namespace cvc5::kind; @@ -47,6 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); } void ExtendedRewriter::setCache(Node n, Node ret) const @@ -1702,19 +1705,50 @@ bool ExtendedRewriter::inferSubstitution(Node n, return false; } -Node ExtendedRewriter::extendedRewriteStrings(Node ret) const +Node ExtendedRewriter::extendedRewriteStrings(Node node) const { - Node new_ret; Trace("q-ext-rewrite-debug") - << "Extended rewrite strings : " << ret << std::endl; + << "Extended rewrite strings : " << node << std::endl; - if (ret.getKind() == EQUAL) + Kind k = node.getKind(); + if (k == EQUAL) { strings::SequencesRewriter sr(&d_rew, nullptr); - new_ret = sr.rewriteEqualityExt(ret); + return sr.rewriteEqualityExt(node); } + else if (k == STRING_SUBSTR) + { + NodeManager* nm = NodeManager::currentNM(); + Node tot_len = d_rew.rewrite(nm->mkNode(STRING_LENGTH, node[0])); + strings::ArithEntail aent(&d_rew); + // (str.substr s x y) --> "" if x < len(s) |= 0 >= y + Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(LT, node[1], tot_len)); + if (aent.checkWithAssumption(n1_lt_tot_len, d_zero, node[2], false)) + { + Node ret = strings::Word::mkEmptyWord(node.getType()); + debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN"); + return ret; + } - return new_ret; + // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s) + Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_zero, node[2])); + if (aent.checkWithAssumption(non_zero_len, node[1], tot_len, false)) + { + Node ret = strings::Word::mkEmptyWord(node.getType()); + debugExtendedRewrite(node, ret, "SS_NON_ZERO_LEN_ENTAILS_OOB"); + return ret; + } + // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s) + Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_zero)); + if (aent.checkWithAssumption(geq_zero_start, d_zero, tot_len, false)) + { + Node ret = strings::Word::mkEmptyWord(node.getType()); + debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S"); + return ret; + } + } + + return Node::null(); } void ExtendedRewriter::debugExtendedRewrite(Node n, diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index b4dcab041..1b9d0dae4 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -259,9 +259,10 @@ class ExtendedRewriter * may be applied as a preprocessing step. */ bool d_aggr; - /** true/false nodes */ + /** Common constant nodes */ Node d_true; Node d_false; + Node d_zero; }; } // namespace quantifiers diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 295afb8c9..6529a81d1 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -96,6 +96,10 @@ class ArithEntail * checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true * * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true + * + * Since this method rewrites on rewriting and may introduce new variables + * (slack variables for inequalities), it should *not* be called from the + * main rewriter of strings, or non-termination can occur. */ bool checkWithAssumption(Node assumption, Node a, @@ -114,6 +118,10 @@ class ArithEntail * checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true * * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true + * + * Since this method rewrites on rewriting and may introduce new variables + * (slack variables for inequalities), it should *not* be called from the + * main rewriter of strings, or non-termination can occur. */ bool checkWithAssumptions(std::vector assumptions, Node a, diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 9887e7ef0..783e258fa 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1813,6 +1813,13 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } + // (str.substr s x x) ---> "" if (str.len s) <= 1 + if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0])) + { + Node ret = Word::mkEmptyWord(node.getType()); + return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z); + } + // symbolic length analysis for (unsigned r = 0; r < 2; r++) { @@ -1847,44 +1854,6 @@ Node SequencesRewriter::rewriteSubstr(Node node) d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt)); } } - - // (str.substr s x y) --> "" if x < len(s) |= 0 >= y - Node n1_lt_tot_len = - d_arithEntail.rewrite(nm->mkNode(kind::LT, node[1], tot_len)); - if (d_arithEntail.checkWithAssumption( - n1_lt_tot_len, zero, node[2], false)) - { - Node ret = Word::mkEmptyWord(node.getType()); - return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN); - } - - // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s) - Node non_zero_len = - d_arithEntail.rewrite(nm->mkNode(kind::LT, zero, node[2])); - if (d_arithEntail.checkWithAssumption( - non_zero_len, node[1], tot_len, false)) - { - Node ret = Word::mkEmptyWord(node.getType()); - return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB); - } - - // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s) - Node geq_zero_start = - d_arithEntail.rewrite(nm->mkNode(kind::GEQ, node[1], zero)); - if (d_arithEntail.checkWithAssumption( - geq_zero_start, zero, tot_len, false)) - { - Node ret = Word::mkEmptyWord(node.getType()); - return returnRewrite( - node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S); - } - - // (str.substr s x x) ---> "" if (str.len s) <= 1 - if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0])) - { - Node ret = Word::mkEmptyWord(node.getType()); - return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z); - } } if (!curr.isNull()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cb535a469..5e64cfcbc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2287,6 +2287,7 @@ set(regress_1_tests regress1/strings/nf-ff-contains-abs.smt2 regress1/strings/no-lazy-pp-quant.smt2 regress1/strings/non_termination_regular_expression4.smt2 + regress1/strings/non-terminating-rewrite-aent.smt2 regress1/strings/norn-13.smt2 regress1/strings/norn-360.smt2 regress1/strings/norn-ab.smt2 diff --git a/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 new file mode 100644 index 000000000..211209255 --- /dev/null +++ b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(assert +(let ((_let_1 (str.len a))) (let ((_let_2 (str.len b))) (let ((_let_3 (+ _let_1 (* (- 1) _let_2)))) (let ((_let_4 (ite (>= _let_3 1) (str.substr a 0 _let_3) (str.substr b 0 (+ (* (- 1) _let_1) _let_2))))) (let ((_let_5 (str.len _let_4))) (let ((_let_6 (str.len c))) (let ((_let_7 (+ _let_6 (* (- 1) _let_5)))) (let ((_let_8 (ite (>= _let_7 0) (str.substr c _let_5 _let_7) (str.substr _let_4 _let_6 (+ (* (- 1) _let_6) _let_5))))) (let ((_let_9 (str.len _let_8))) (let ((_let_10 (ite (>= _let_1 _let_9) (str.substr a _let_9 (- _let_1 _let_9)) (str.substr _let_8 _let_1 (- _let_9 _let_1))))) (and (= _let_8 (str.++ a _let_10)) (not (= "" _let_10)) (>= (str.len _let_10) 1)))))))))))) +) +(check-sat) diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 32122e619..bcac315a7 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -248,8 +248,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) a, d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "A" (+ x (str.len s2)) x) -> "" n = d_nodeManager->mkNode( @@ -258,8 +257,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) d_nodeManager->mkNode( kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "A" x y) -> (str.substr "A" x y) n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y); @@ -271,14 +269,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) abcd, d_nodeManager->mkNode(kind::PLUS, x, three), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) n = d_nodeManager->mkNode( kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x); res = sr.rewriteSubstr(n); - ASSERT_EQ(res, n); + sameNormalForm(res, n); // (str.substr (str.substr s x x) x x) -> "" n = d_nodeManager->mkNode(kind::STRING_SUBSTR, -- 2.30.2