summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-12-01 00:31:17 -0800
committerAndres Noetzli <andres.noetzli@gmail.com>2018-12-01 00:31:17 -0800
commita42ec6d1f634cf4a3a8670aac5d95ac9d51fef48 (patch)
treeab9db8ffabcf5e530d5a9c41757fa285941ea6fd
parent41b38de8b059d346764cd5ca112740aa09e1d163 (diff)
one weird rewriteoneWeirdRewrite
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp16
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback