diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-15 08:39:02 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-15 10:39:02 -0500 |
commit | de7798ebbc351046d7b5ae7e6379ffd61be0f1c4 (patch) | |
tree | 643add8a3bd72072bda3e777c2fa973e34ea5c9e /src/theory/strings | |
parent | 4298cdaa096cd420c87c9af9f20a8b880fe2d25c (diff) |
Add more (str.replace x y z) rewrites (#2628)
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 154 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 23 |
2 files changed, 138 insertions, 39 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 407279d22..e8a11e62e 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1651,6 +1651,28 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-start-geq-len"); } } + else if (node[0].getKind() == STRING_STRREPL) + { + // (str.substr (str.replace x y z) 0 n) + // ---> (str.replace (str.substr x 0 n) y z) + // if (str.len y) = 1 and (str.len z) = 1 + if (node[1] == zero) + { + Node one = nm->mkConst(Rational(1)); + Node n1len = nm->mkNode(kind::STRING_LENGTH, node[0][1]); + Node n2len = nm->mkNode(kind::STRING_LENGTH, node[0][2]); + if (checkEntailArith(one, n1len) && checkEntailArith(one, n2len) + && checkEntailNonEmpty(node[0][1]) && checkEntailNonEmpty(node[0][2])) + { + Node ret = nm->mkNode( + kind::STRING_STRREPL, + nm->mkNode(kind::STRING_SUBSTR, node[0][0], node[1], node[2]), + node[0][1], + node[0][2]); + return returnRewrite(node, ret, "substr-repl-swap"); + } + } + } std::vector<Node> n1; getConcat(node[0], n1); @@ -2140,6 +2162,16 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn"); } } + + // (str.contains (str.replace x y z) z) ---> + // (or (str.contains x y) (str.contains x z)) + if (node[0][2] == node[1]) + { + Node ret = nm->mkNode(OR, + nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]), + nm->mkNode(STRING_STRCTN, node[0][0], node[0][2])); + return returnRewrite(node, ret, "ctn-repl-to-ctn-disj"); + } } if (node[1].getKind() == kind::STRING_STRREPL) @@ -2439,6 +2471,31 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { return returnRewrite(node, node[0], "rpl-rpl-len-id"); } + + // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x) + // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "") + if (checkEntailArith(nm->mkConst(Rational(1)), l0)) + { + Node empty = nm->mkConst(String("")); + Node rn1 = Rewriter::rewrite( + rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); + if (rn1 != node[1]) + { + std::vector<Node> emptyNodes; + bool allEmptyEqs; + std::tie(allEmptyEqs, emptyNodes) = collectEmptyEqs(rn1); + + if (allEmptyEqs) + { + Node nn1 = mkConcat(STRING_CONCAT, emptyNodes); + if (node[1] != nn1) + { + Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]); + return returnRewrite(node, ret, "rpl-x-y-x-simp"); + } + } + } + } } std::vector<Node> children1; @@ -2511,45 +2568,9 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // Node empty = nm->mkConst(::CVC4::String("")); - // Collect the equalities of the form (= x "") (sorted) - std::set<TNode> emptyNodes; - bool allEmptyEqs = true; - if (cmp_conr.getKind() == kind::EQUAL) - { - if (cmp_conr[0] == empty) - { - emptyNodes.insert(cmp_conr[1]); - } - else if (cmp_conr[1] == empty) - { - emptyNodes.insert(cmp_conr[0]); - } - else - { - allEmptyEqs = false; - } - } - else - { - for (const Node& c : cmp_conr) - { - if (c.getKind() == kind::EQUAL) - { - if (c[0] == empty) - { - emptyNodes.insert(c[1]); - } - else if (c[1] == empty) - { - emptyNodes.insert(c[0]); - } - } - else - { - allEmptyEqs = false; - } - } - } + std::vector<Node> emptyNodes; + bool allEmptyEqs; + std::tie(allEmptyEqs, emptyNodes) = collectEmptyEqs(cmp_conr); if (emptyNodes.size() > 0) { @@ -4761,6 +4782,61 @@ Node TheoryStringsRewriter::inferEqsFromContains(Node x, Node y) return nb.constructNode(); } +std::pair<bool, std::vector<Node> > TheoryStringsRewriter::collectEmptyEqs( + Node x) +{ + NodeManager* nm = NodeManager::currentNM(); + Node empty = nm->mkConst(::CVC4::String("")); + + // Collect the equalities of the form (= x "") (sorted) + std::set<TNode> emptyNodes; + bool allEmptyEqs = true; + if (x.getKind() == kind::EQUAL) + { + if (x[0] == empty) + { + emptyNodes.insert(x[1]); + } + else if (x[1] == empty) + { + emptyNodes.insert(x[0]); + } + else + { + allEmptyEqs = false; + } + } + else + { + for (const Node& c : x) + { + if (c.getKind() == kind::EQUAL) + { + if (c[0] == empty) + { + emptyNodes.insert(c[1]); + } + else if (c[1] == empty) + { + emptyNodes.insert(c[0]); + } + } + else + { + allEmptyEqs = false; + } + } + } + + if (emptyNodes.size() == 0) + { + allEmptyEqs = false; + } + + return std::make_pair( + allEmptyEqs, std::vector<Node>(emptyNodes.begin(), emptyNodes.end())); +} + Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index ed42ce762..2c38ce8dc 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -18,6 +18,9 @@ #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H +#include <utility> +#include <vector> + #include "theory/rewriter.h" #include "theory/type_enumerator.h" #include "expr/attribute.h" @@ -632,6 +635,26 @@ class TheoryStringsRewriter { * infer that any of the yi must be empty. */ static Node inferEqsFromContains(Node x, Node y); + + /** + * Collects equal-to-empty nodes from a conjunction or a single + * node. Returns a list of nodes that are compared to empty nodes + * and a boolean that indicates whether all nodes in the + * conjunction were a comparison with the empty node. The nodes in + * the list are sorted and duplicates removed. + * + * Examples: + * + * collectEmptyEqs( (= "" x) ) = { true, [x] } + * collectEmptyEqs( (and (= "" x) (= "" y)) ) = { true, [x, y] } + * collectEmptyEqs( (and (= "A" x) (= "" y) (= "" y)) ) = { false, [y] } + * + * @param x The conjunction of equalities or a single equality + * @return A pair of a boolean that indicates whether the + * conjunction consists only of comparisons to the empty string + * and the list of nodes that are compared to the empty string + */ + static std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x); };/* class TheoryStringsRewriter */ }/* CVC4::theory::strings namespace */ |