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

fix #5074, add rewrite rules to simplify indexof special cases

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-06 12:35:15 -08:00
parent e8b3c90e14
commit e83f31949e
2 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_axioms.cpp
View file

@ -420,7 +420,7 @@ namespace seq {
expr_ref cnt(seq.str.mk_contains(t, s), m);
expr_ref i_eq_m1 = mk_eq(i, minus_one);
expr_ref i_eq_0 = mk_eq(i, zero);
expr_ref s_eq_empty = mk_eq_empty(s);
expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort()));
expr_ref t_eq_empty = mk_eq_empty(t);
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1

13
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1578,6 +1578,7 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
indexof(s, b, c) -> -1 if c < 0
indexof(a, "", 0) -> if a = "" then 0 else -1
indexof("", b, r) -> if b = "" and r = 0 then 0 else -1
indexof(a, "", x) -> if 0 <= x <= len(a) then x else - 1
indexof(unit(x)+a, b, r+1) -> indexof(a, b, r)
indexof(unit(x)+a, unit(y)+b, 0) -> indexof(a,unit(y)+b, 0) if x != y
indexof(substr(x,y,len1), z, len2) -> -1 if len2 > len1
@ -1591,11 +1592,11 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
int idx = s1.indexofu(s2, r.get_unsigned());
result = m_autil.mk_numeral(rational(idx), true);
result = m_autil.mk_int(idx);
return BR_DONE;
}
if (m_autil.is_numeral(c, r) && r.is_neg()) {
result = m_autil.mk_numeral(rational(-1), true);
result = m_autil.mk_int(-1);
return BR_DONE;
}
@ -1604,6 +1605,14 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
return BR_DONE;
}
if (str().is_empty(b)) {
result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), c),
m_autil.mk_le(c, str().mk_length(a))),
c,
m_autil.mk_int(-1));
return BR_REWRITE2;
}
if (str().is_empty(a)) {
expr* emp = str().mk_is_empty(b);