mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #1959

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-20 20:17:09 -08:00
parent c95dbb47a3
commit 90070fda95
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_seq.cpp
View file

@ -4823,6 +4823,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
/*
0 <= i <= len(s) => s = xe & i = len(x)
i < 0 => len(e) = 0
i > len(s) => len(e) = 0
*/
void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
expr_ref x(mk_skolem(m_pre, s, i), m);
@ -4830,11 +4831,13 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref xe = mk_concat(x, e);
literal le_is_0 = mk_eq(zero, m_util.str.mk_length(e), false);
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));
add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx, false));
add_axiom(i_ge_0, mk_eq(zero, m_util.str.mk_length(e), false));
add_axiom(i_ge_0, le_is_0);
add_axiom(i_le_s, le_is_0);
}