From: Andres Noetzli Date: Fri, 18 Jan 2019 13:59:09 +0000 (-0800) Subject: Strings: Introduce checkEntailContains() (#2809) X-Git-Tag: cvc5-1.0.0~4278 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a5e007ea530c97c5f3885958f5d018e350013a7;p=cvc5.git Strings: Introduce checkEntailContains() (#2809) --- diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b4c80e55b..e57403250 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -238,18 +238,11 @@ Node TheoryStringsRewriter::rewriteEquality(Node node) // ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false ) for (unsigned r = 0; r < 2; r++) { - Node ctn = NodeManager::currentNM()->mkNode( - kind::STRING_STRCTN, node[r], node[1 - r]); // must call rewrite contains directly to avoid infinite loop // we do a fix point since we may rewrite contains terms to simpler // contains terms. - Node prev; - do - { - prev = ctn; - ctn = rewriteContains(ctn); - } while (prev != ctn && ctn.getKind() == kind::STRING_STRCTN); - if (ctn.isConst()) + Node ctn = checkEntailContains(node[r], node[1 - r], false); + if (!ctn.isNull()) { if (!ctn.getConst()) { @@ -1921,9 +1914,8 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } else if (node[0].getKind() == STRING_STRREPL) { - Node rplDomain = nm->mkNode(STRING_STRCTN, node[0][1], node[1]); - rplDomain = Rewriter::rewrite(rplDomain); - if (rplDomain.isConst() && !rplDomain.getConst()) + Node rplDomain = checkEntailContains(node[0][1], node[1]); + if (!rplDomain.isNull() && !rplDomain.getConst()) { Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]); Node d2 = @@ -1975,15 +1967,11 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { // replacement does not change y. (str.contains x w) checks that if the // replacement changes anything in y, the w makes it impossible for it to // occur in x. - Node ctnUnchanged = nm->mkNode(kind::STRING_STRCTN, node[0], n[0]); - Node ctnUnchangedR = Rewriter::rewrite(ctnUnchanged); - - if (ctnUnchangedR.isConst() && !ctnUnchangedR.getConst()) + Node ctnConst = checkEntailContains(node[0], n[0]); + if (!ctnConst.isNull() && !ctnConst.getConst()) { - Node ctnChange = nm->mkNode(kind::STRING_STRCTN, node[0], n[2]); - Node ctnChangeR = Rewriter::rewrite(ctnChange); - - if (ctnChangeR.isConst() && !ctnChangeR.getConst()) + Node ctnConst2 = checkEntailContains(node[0], n[2]); + if (!ctnConst2.isNull() && !ctnConst2.getConst()) { Node res = nm->mkConst(false); return returnRewrite(node, res, "ctn-rpl-non-ctn"); @@ -2211,9 +2199,8 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { // if (str.contains z w) ---> false and (str.len w) = 1 if (checkEntailLengthOne(node[1])) { - Node ctn = Rewriter::rewrite( - nm->mkNode(kind::STRING_STRCTN, node[1], node[0][2])); - if (ctn.isConst() && !ctn.getConst()) + Node ctn = checkEntailContains(node[1], node[0][2]); + if (!ctn.isNull() && !ctn.getConst()) { Node empty = nm->mkConst(String("")); Node ret = nm->mkNode( @@ -2353,14 +2340,13 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { fstr = Rewriter::rewrite(fstr); } - Node cmp_con = nm->mkNode(kind::STRING_STRCTN, fstr, node[1]); - Trace("strings-rewrite-debug") - << "For " << node << ", check " << cmp_con << std::endl; - Node cmp_conr = Rewriter::rewrite(cmp_con); + Node cmp_conr = checkEntailContains(fstr, node[1]); + Trace("strings-rewrite-debug") << "For " << node << ", check contains(" + << fstr << ", " << node[1] << ")" << std::endl; Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl; std::vector children1; getConcat(node[1], children1); - if (cmp_conr.isConst()) + if (!cmp_conr.isNull()) { if (cmp_conr.getConst()) { @@ -2551,10 +2537,9 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { getConcat(node[1], children1); // check if contains definitely does (or does not) hold - Node cmp_con = - NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, node[0], node[1]); + Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]); Node cmp_conr = Rewriter::rewrite(cmp_con); - if (cmp_conr.isConst()) + if (!checkEntailContains(node[0], node[1]).isNull()) { if (cmp_conr.getConst()) { @@ -2781,9 +2766,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return returnRewrite(node, node[0], "repl-repl2-inv-id"); } bool dualReplIteSuccess = false; - Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]); - cmp_con = Rewriter::rewrite(cmp_con); - if (cmp_con.isConst() && !cmp_con.getConst()) + Node cmp_con = checkEntailContains(node[1][0], node[1][2]); + if (!cmp_con.isNull() && !cmp_con.getConst()) { // str.contains( x, z ) ---> false // implies @@ -2797,13 +2781,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // implies // str.replace( x, str.replace( x, y, z ), w ) ---> // ite( str.contains( x, y ), x, w ) - cmp_con = nm->mkNode(STRING_STRCTN, node[1][1], node[1][2]); - cmp_con = Rewriter::rewrite(cmp_con); - if (cmp_con.isConst() && !cmp_con.getConst()) + cmp_con = checkEntailContains(node[1][1], node[1][2]); + if (!cmp_con.isNull() && !cmp_con.getConst()) { - cmp_con = nm->mkNode(STRING_STRCTN, node[1][2], node[1][1]); - cmp_con = Rewriter::rewrite(cmp_con); - if (cmp_con.isConst() && !cmp_con.getConst()) + cmp_con = checkEntailContains(node[1][2], node[1][1]); + if (!cmp_con.isNull() && !cmp_con.getConst()) { dualReplIteSuccess = true; } @@ -2832,9 +2814,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(y, z) ----> false and ( y == w or x == w ) implies // implies // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w) - Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]); - cmp_con = Rewriter::rewrite(cmp_con); - invSuccess = cmp_con.isConst() && !cmp_con.getConst(); + Node cmp_con = checkEntailContains(node[1][0], node[1][2]); + invSuccess = !cmp_con.isNull() && !cmp_con.getConst(); } } else @@ -2842,13 +2823,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(x, z) ----> false and str.contains(x, w) ----> false // implies // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u) - Node cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][1]); - cmp_con = Rewriter::rewrite(cmp_con); - if (cmp_con.isConst() && !cmp_con.getConst()) + Node cmp_con = checkEntailContains(node[0], node[1][1]); + if (!cmp_con.isNull() && !cmp_con.getConst()) { - cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][2]); - cmp_con = Rewriter::rewrite(cmp_con); - invSuccess = cmp_con.isConst() && !cmp_con.getConst(); + cmp_con = checkEntailContains(node[0], node[1][2]); + invSuccess = !cmp_con.isNull() && !cmp_con.getConst(); } } if (invSuccess) @@ -2863,9 +2842,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { // str.contains( z, w ) ----> false implies // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z ) - Node cmp_con = nm->mkNode(STRING_STRCTN, node[1], node[2][0]); - cmp_con = Rewriter::rewrite(cmp_con); - if (cmp_con.isConst() && !cmp_con.getConst()) + Node cmp_con = checkEntailContains(node[1], node[2][0]); + if (!cmp_con.isNull() && !cmp_con.getConst()) { Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]); @@ -2884,9 +2862,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { // str.contains( x, z ) ----> false implies // str.replace( x, y, str.replace( y, z, w ) ) ---> x - cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[2][1]); - cmp_con = Rewriter::rewrite(cmp_con); - success = cmp_con.isConst() && !cmp_con.getConst(); + cmp_con = checkEntailContains(node[0], node[2][1]); + success = !cmp_con.isNull() && !cmp_con.getConst(); } if (success) { @@ -2911,9 +2888,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { checkLhs.end(), children0.begin(), children0.begin() + checkIndex); Node lhs = mkConcat(STRING_CONCAT, checkLhs); Node rhs = children0[checkIndex]; - Node ctn = nm->mkNode(STRING_STRCTN, lhs, rhs); - ctn = Rewriter::rewrite(ctn); - if (ctn.isConst() && ctn.getConst()) + Node ctn = checkEntailContains(lhs, rhs); + if (!ctn.isNull() && ctn.getConst()) { lastLhs = lhs; lastCheckIndex = checkIndex; @@ -3672,12 +3648,11 @@ bool TheoryStringsRewriter::componentContainsBase( { // (str.contains (str.replace x y z) w) ---> true // if (str.contains x w) --> true and (str.contains z w) ---> true - Node xCtnW = Rewriter::rewrite(nm->mkNode(STRING_STRCTN, n1[0], n2)); - if (xCtnW.isConst() && xCtnW.getConst()) + Node xCtnW = checkEntailContains(n1[0], n2); + if (!xCtnW.isNull() && xCtnW.getConst()) { - Node zCtnW = - Rewriter::rewrite(nm->mkNode(STRING_STRCTN, n1[2], n2)); - if (zCtnW.isConst() && zCtnW.getConst()) + Node zCtnW = checkEntailContains(n1[2], n2); + if (!zCtnW.isNull() && zCtnW.getConst()) { return true; } @@ -3940,6 +3915,31 @@ Node TheoryStringsRewriter::lengthPreserveRewrite(Node n) return res.isNull() ? n : res; } +Node TheoryStringsRewriter::checkEntailContains(Node a, + Node b, + bool fullRewriter) +{ + NodeManager* nm = NodeManager::currentNM(); + Node ctn = nm->mkNode(kind::STRING_STRCTN, a, b); + + if (fullRewriter) + { + ctn = Rewriter::rewrite(ctn); + } + else + { + Node prev; + do + { + prev = ctn; + ctn = rewriteContains(ctn); + } while (prev != ctn && ctn.getKind() == kind::STRING_STRCTN); + } + + Assert(ctn.getType().isBoolean()); + return ctn.isConst() ? ctn : Node::null(); +} + bool TheoryStringsRewriter::checkEntailNonEmpty(Node a) { Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 69d6ff68e..e4b76036d 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -461,6 +461,19 @@ class TheoryStringsRewriter { */ static Node lengthPreserveRewrite(Node n); + /** + * Checks whether a string term `a` is entailed to contain or not contain a + * string term `b`. + * + * @param a The string that is checked whether it contains `b` + * @param b The string that is checked whether it is contained in `a` + * @param fullRewriter Determines whether the function can use the full + * rewriter or only `rewriteContains()` (useful for avoiding loops) + * @return true node if it can be shown that `a` contains `b`, false node if + * it can be shown that `a` does not contain `b`, null node otherwise + */ + static Node checkEntailContains(Node a, Node b, bool fullRewriter = false); + /** entail non-empty * * Checks whether string a is entailed to be non-empty. Is equivalent to