mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge pull request #2170 from mtrberzi/issue2092

Browse source 
z3str3: fix str.indexof with offset (issue #2092)
This commit is contained in:
Nikolaj Bjorner 2019-03-06 17:36:46 -08:00 committed by GitHub
parent de7731fd22 e05596e7e5
commit 65f0da9806
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str.cpp
View file

@ -1427,7 +1427,7 @@ namespace smt {
// 0 < i < len(H) -->
// H = hd ++ tl
// len(hd) = i
// str.indexof(tl, N, 0)
// i + str.indexof(tl, N, 0)
expr * H = nullptr; // "haystack"
expr * N = nullptr; // "needle"
@ -1463,12 +1463,19 @@ namespace smt {
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
assert_implication(premise, conclusion);
}
// case 4: 0 < i < len(H)
// case 3.5: H doesn't contain N
{
expr_ref premise(m.mk_not(u.str.mk_contains(H, N)), m);
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
assert_implication(premise, conclusion);
}
// case 4: 0 < i < len(H) and H contains N
{
expr_ref premise1(m_autil.mk_gt(i, zero), m);
//expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
expr_ref premise2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m);
expr_ref _premise(m.mk_and(premise1, premise2), m);
expr_ref premise3(u.str.mk_contains(H, N), m);
expr_ref _premise(m.mk_and(premise1, premise2, premise3), m);
expr_ref premise(_premise);
th_rewriter rw(m);
rw(premise);
@ -1479,7 +1486,8 @@ namespace smt {
expr_ref_vector conclusion_terms(m);
conclusion_terms.push_back(ctx.mk_eq_atom(H, mk_concat(hd, tl)));
conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(hd), i));
conclusion_terms.push_back(ctx.mk_eq_atom(e, mk_indexof(tl, N)));
conclusion_terms.push_back(u.str.mk_contains(tl, N));
conclusion_terms.push_back(ctx.mk_eq_atom(e, m_autil.mk_add(i, mk_indexof(tl, N))));
expr_ref conclusion(mk_and(conclusion_terms), m);
assert_implication(premise, conclusion);