diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-19 12:12:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-19 17:12:28 +0000 |
commit | bcb536ef60cb24c19001c0efbde55ff3a37e114f (patch) | |
tree | 1a9605630ff2ea9bf5099fdb20e795c09e88caf9 /src | |
parent | 29aac1b9d886e245a7b5cd2122d7b80fa230152d (diff) |
Fix positive contains indexof rewrites for empty string second argument (#6566)
Fixes #6560.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 41 |
1 files changed, 24 insertions, 17 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index ff718c124..1577a5625 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2452,23 +2452,30 @@ Node SequencesRewriter::rewriteIndexof(Node node) return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS); } } - - // strip symbolic length - Node new_len = node[2]; - std::vector<Node> nr; - if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len)) - { - // For example: - // z>str.len( x1 ) and str.contains( x2, y )-->true - // implies - // str.indexof( str.++( x1, x2 ), y, z ) ---> - // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) ) - Node nn = utils::mkConcat(children0, stype); - Node ret = - nm->mkNode(kind::PLUS, - nm->mkNode(kind::MINUS, node[2], new_len), - nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len)); - return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN); + // To show that the first argument definitely contains the second, the + // index must be a valid index in the first argument. This ensures that + // (str.indexof t "" n) is not rewritten to something other than -1 when n + // is beyond the length of t. This is not required for the above rewrites, + // which only apply when n=0. + if (ArithEntail::check(node[2]) && ArithEntail::check(len0, node[2])) + { + // strip symbolic length + Node new_len = node[2]; + std::vector<Node> nr; + if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len)) + { + // For example: + // z>=0 and z>str.len( x1 ) and str.contains( x2, y )-->true + // implies + // str.indexof( str.++( x1, x2 ), y, z ) ---> + // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) ) + Node nn = utils::mkConcat(children0, stype); + Node ret = + nm->mkNode(PLUS, + nm->mkNode(MINUS, node[2], new_len), + nm->mkNode(STRING_STRIDOF, nn, node[1], new_len)); + return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN); + } } } else |