mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

fix part 1 of #875

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-25 18:09:27 -08:00
parent 1bfd09e16b
commit 777091e653
2 changed files with 17 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -2031,11 +2031,13 @@ namespace smt {
v.shrink(old_size); v.shrink(old_size);
} }
#if 0
void context::mark_as_deleted(clause * cls) { void context::mark_as_deleted(clause * cls) {
SASSERT(!cls->deleted()); SASSERT(!cls->deleted());
remove_cls_occs(cls); remove_cls_occs(cls);
cls->mark_as_deleted(m_manager); cls->mark_as_deleted(m_manager);
} }
#endif
/** /**
\brief Undo variable assignments. \brief Undo variable assignments.

28
src/smt/theory_seq.cpp
View file

@ -2958,22 +2958,19 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
let i = Index(t, s, offset): let i = Index(t, s, offset):
offset >= len(t) => i = -1 offset >= len(t) => i = -1
offset fixed to 0:
len(t) != 0 & !contains(t, s) => i = -1 len(t) != 0 & !contains(t, s) => i = -1
len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
tightest_prefix(x, s) tightest_prefix(x, s)
offset not fixed:
0 <= offset < len(t) => xy = t & 0 <= offset < len(t) => xy = t &
len(x) = offset & len(x) = offset &
(-1 = indexof(y, s, 0) => -1 = i) & (-1 = indexof(y, s, 0) => -1 = i) &
(indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i) (indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i)
if offset < 0 offset < 0 => i = -1
under specified
optional lemmas: optional lemmas:
(len(s) > len(t) -> i = -1) (len(s) > len(t) -> i = -1)
@ -2987,17 +2984,19 @@ void theory_seq::add_indexof_axiom(expr* i) {
expr_ref minus_one(m_autil.mk_int(-1), m); expr_ref minus_one(m_autil.mk_int(-1), m);
expr_ref zero(m_autil.mk_int(0), m); expr_ref zero(m_autil.mk_int(0), m);
expr_ref xsy(m); expr_ref xsy(m);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal i_eq_m1 = mk_eq(i, minus_one, false);
add_axiom(cnt, i_eq_m1);
literal s_eq_empty = mk_eq_empty(s);
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), i_eq_m1);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) { if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
expr_ref x = mk_skolem(m_indexof_left, t, s); expr_ref x = mk_skolem(m_indexof_left, t, s);
expr_ref y = mk_skolem(m_indexof_right, t, s); expr_ref y = mk_skolem(m_indexof_right, t, s);
xsy = mk_concat(x, s, y); xsy = mk_concat(x, s, y);
expr_ref lenx(m_util.str.mk_length(x), m); expr_ref lenx(m_util.str.mk_length(x), m);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal s_eq_empty = mk_eq_empty(s);
add_axiom(cnt, mk_eq(i, minus_one, false));
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false)); add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
tightest_prefix(s, x); tightest_prefix(s, x);
@ -3024,10 +3023,13 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y))); add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false)); add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
add_axiom(~offset_ge_0, offset_ge_len, add_axiom(~offset_ge_0, offset_ge_len,
~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false)); ~mk_eq(indexof0, minus_one, false), i_eq_m1);
add_axiom(~offset_ge_0, offset_ge_len, add_axiom(~offset_ge_0, offset_ge_len,
~mk_literal(m_autil.mk_ge(indexof0, zero)), ~mk_literal(m_autil.mk_ge(indexof0, zero)),
mk_eq(offset_p_indexof0, i, false)); mk_eq(offset_p_indexof0, i, false));
// offset < 0 => -1 = i
add_axiom(offset_ge_0, i_eq_m1);
} }
} }