diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7e5f7102d..6a9648311 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1545,6 +1545,35 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { return returnRewrite(node, res, "ctn-rpl-non-ctn"); } } + + // (str.contains x (str.++ w (str.replace x y x) z)) ---> + // (and (= w "") (= x (str.replace x y x)) (= z "")) + if (node[0] == n[0] && node[0] == n[2]) + { + Node ret; + if (nc2.size() > 1) + { + Node emp = nm->mkConst(CVC4::String("")); + NodeBuilder<> nb(kind::AND); + for (const Node& n2 : nc2) + { + if (n2 == n) + { + nb << nm->mkNode(kind::EQUAL, node[0], node[1]); + } + else + { + nb << nm->mkNode(kind::EQUAL, emp, n2); + } + } + ret = nb.constructNode(); + } + else + { + ret = nm->mkNode(kind::EQUAL, node[0], node[1]); + } + return returnRewrite(node, ret, "ctn-repl-self"); + } } } @@ -1749,6 +1778,41 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } } + if (node[0].getKind() == kind::STRING_SUBSTR) + { + // (str.contains (str.substr x n (str.len y)) y) ---> + // (= (str.substr x n (str.len y)) y) + // + // TODO: generalize with over-/underapproximation to: + // + // (str.contains x y) ---> (= x y) if (<= (str.len x) (str.len y)) + if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1])) + { + Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]); + return returnRewrite(node, ret, "ctn-substr"); + } + } + + if (node[1].getKind() == kind::STRING_STRREPL) + { + // (str.contains x (str.replace y x y)) ---> + // (str.contains x y) + if (node[0] == node[1][1] && node[1][0] == node[1][2]) + { + Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]); + return returnRewrite(node, ret, "ctn-repl"); + } + + // (str.contains x (str.replace "" x y)) ---> + // (= "" (str.replace "" x y)) + Node emp = nm->mkConst(CVC4::String("")); + if (node[0] == node[1][1] && node[1][0] == emp) + { + Node ret = nm->mkNode(kind::EQUAL, emp, node[1]); + return returnRewrite(node, ret, "ctn-repl-empty"); + } + } + Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } |