mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

z3str3: fix str.indexof with offset (issue #2092)

Browse source
This commit is contained in:
Murphy Berzish 2019-03-06 11:41:56 -05:00
parent f00697cf95
commit e05596e7e5
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) --> // 0 < i < len(H) -->
// H = hd ++ tl // H = hd ++ tl
// len(hd) = i // len(hd) = i
// str.indexof(tl, N, 0) // i + str.indexof(tl, N, 0)
expr * H = nullptr; // "haystack" expr * H = nullptr; // "haystack"
expr * N = nullptr; // "needle" expr * N = nullptr; // "needle"
@ -1463,12 +1463,19 @@ namespace smt {
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
assert_implication(premise, conclusion); 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 premise1(m_autil.mk_gt(i, zero), m);
//expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), 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 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); expr_ref premise(_premise);
th_rewriter rw(m); th_rewriter rw(m);
rw(premise); rw(premise);
@ -1479,7 +1486,8 @@ namespace smt {
expr_ref_vector conclusion_terms(m); 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(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(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); expr_ref conclusion(mk_and(conclusion_terms), m);
assert_implication(premise, conclusion); assert_implication(premise, conclusion);