diff options
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 126 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 13 |
2 files changed, 76 insertions, 63 deletions
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<bool>()) { @@ -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<bool>()) + Node rplDomain = checkEntailContains(node[0][1], node[1]); + if (!rplDomain.isNull() && !rplDomain.getConst<bool>()) { 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<bool>()) + Node ctnConst = checkEntailContains(node[0], n[0]); + if (!ctnConst.isNull() && !ctnConst.getConst<bool>()) { - Node ctnChange = nm->mkNode(kind::STRING_STRCTN, node[0], n[2]); - Node ctnChangeR = Rewriter::rewrite(ctnChange); - - if (ctnChangeR.isConst() && !ctnChangeR.getConst<bool>()) + Node ctnConst2 = checkEntailContains(node[0], n[2]); + if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>()) { 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<bool>()) + Node ctn = checkEntailContains(node[1], node[0][2]); + if (!ctn.isNull() && !ctn.getConst<bool>()) { 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<Node> children1; getConcat(node[1], children1); - if (cmp_conr.isConst()) + if (!cmp_conr.isNull()) { if (cmp_conr.getConst<bool>()) { @@ -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<bool>()) { @@ -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<bool>()) + Node cmp_con = checkEntailContains(node[1][0], node[1][2]); + if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) { // 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<bool>()) + cmp_con = checkEntailContains(node[1][1], node[1][2]); + if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) { - 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<bool>()) + cmp_con = checkEntailContains(node[1][2], node[1][1]); + if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) { 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<bool>(); + Node cmp_con = checkEntailContains(node[1][0], node[1][2]); + invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); } } 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<bool>()) + Node cmp_con = checkEntailContains(node[0], node[1][1]); + if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) { - cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][2]); - cmp_con = Rewriter::rewrite(cmp_con); - invSuccess = cmp_con.isConst() && !cmp_con.getConst<bool>(); + cmp_con = checkEntailContains(node[0], node[1][2]); + invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); } } 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<bool>()) + Node cmp_con = checkEntailContains(node[1], node[2][0]); + if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) { 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<bool>(); + cmp_con = checkEntailContains(node[0], node[2][1]); + success = !cmp_con.isNull() && !cmp_con.getConst<bool>(); } 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<bool>()) + Node ctn = checkEntailContains(lhs, rhs); + if (!ctn.isNull() && ctn.getConst<bool>()) { 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<bool>()) + Node xCtnW = checkEntailContains(n1[0], n2); + if (!xCtnW.isNull() && xCtnW.getConst<bool>()) { - Node zCtnW = - Rewriter::rewrite(nm->mkNode(STRING_STRCTN, n1[2], n2)); - if (zCtnW.isConst() && zCtnW.getConst<bool>()) + Node zCtnW = checkEntailContains(n1[2], n2); + if (!zCtnW.isNull() && zCtnW.getConst<bool>()) { 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 |