diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-01 00:31:17 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-01 00:31:17 -0800 |
commit | a42ec6d1f634cf4a3a8670aac5d95ac9d51fef48 (patch) | |
tree | ab9db8ffabcf5e530d5a9c41757fa285941ea6fd | |
parent | 41b38de8b059d346764cd5ca112740aa09e1d163 (diff) |
one weird rewriteoneWeirdRewrite
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 0de42f686..593f42544 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1670,6 +1670,22 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Node ret = nm->mkConst(::CVC4::String("")); return returnRewrite(node, ret, "ss-start-geq-len"); } + + if (node[0][2].getKind() == STRING_STRIDOF) + { + if (checkEntailArith(node[1], node[0][2][2], true)) + { + Node nidof = + nm->mkNode(STRING_STRIDOF, node[0][2][0], node[0][2][1], node[1]); + Node nlen = node[2].substitute(TNode(node[0][2]), TNode(nidof)); + Node ret = + nm->mkNode(STRING_SUBSTR, + nm->mkNode(STRING_SUBSTR, node[0][0], node[0][1], nidof), + node[1], + nlen); + return returnRewrite(node, ret, "ss-inc-idof-start-idx"); + } + } } else if (node[0].getKind() == STRING_STRREPL) { |