diff options
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 41 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue6560-indexof-reduction.smt2 | 7 |
3 files changed, 32 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 84ed52991..21a9f04b8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1131,6 +1131,7 @@ set(regress_0_tests regress0/strings/issue6203-3-unfold-trivial-true.smt2 regress0/strings/issue6510-seq-bool.smt2 regress0/strings/issue6520.smt2 + regress0/strings/issue6560-indexof-reduction.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6560-indexof-reduction.smt2 b/test/regress/regress0/strings/issue6560-indexof-reduction.smt2 new file mode 100644 index 000000000..bdb9d2877 --- /dev/null +++ b/test/regress/regress0/strings/issue6560-indexof-reduction.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () String) +(assert (> (str.indexof a "" (* 2 (str.len a))) 0)) +(check-sat) |