diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-18 19:13:04 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-18 19:13:04 -0800 |
commit | 36beb4399234e2a9cba6f953e7b09498cc281dc8 (patch) | |
tree | 15d139d8c07f5f05c044ccfa13ba379fc101adcb | |
parent | 9e581134ef9badf8e17dc9fc0586638a97e68148 (diff) |
more rewriteskindSkolems
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 3b1fd6a33..89070a0b6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1582,9 +1582,28 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = nm->mkNode(STRING_SK_PREFIX, node[0][0], node[1]); } + else if (node[0].getKind() == STRING_CONCAT) + { + std::vector<Node> nvec; + utils::getConcat(node[0], nvec); + + Node curr = node[1]; + std::vector<Node> nres; + if (stripSymbolicLength(nvec, nres, 1, curr)) + { + retNode = nm->mkNode(STRING_CONCAT, utils::mkConcat(STRING_CONCAT, nres), nm->mkNode( + STRING_SK_PREFIX, utils::mkConcat(STRING_CONCAT, nvec), curr)); + } + } + + if (node[1] == nm->mkConst(Rational(0))) + { + retNode = nm->mkConst(String()); + } } else if (nk == STRING_SK_SUFFIX) { + // std::cout << node << std::endl; if (node[0].isConst() && node[1].isConst()) { String s = node[0].getConst<String>(); @@ -1598,6 +1617,28 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = nm->mkConst(String()); } + else if (node[0].getKind() == STRING_SK_SUFFIX) + { + retNode = nm->mkNode( + STRING_SK_SUFFIX, node[0][0], nm->mkNode(PLUS, node[1], node[0][1])); + } + else if (node[0].getKind() == STRING_CONCAT) + { + std::vector<Node> nvec; + utils::getConcat(node[0], nvec); + + Node curr = node[1]; + std::vector<Node> nres; + if (stripSymbolicLength(nvec, nres, 1, curr)) { + retNode = nm->mkNode( + STRING_SK_SUFFIX, utils::mkConcat(STRING_CONCAT, nvec), curr); + } + } + + if (node[1] == nm->mkConst(Rational(0))) + { + retNode = node[0]; + } } else if (nk == STRING_SK_FIRST_CTN_PRE) { |