mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fixing #2956

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 19:58:13 -07:00
parent 41965acaf1
commit e075f38152
1 changed files with 8 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/theory_seq.cpp
View file

@ -5723,19 +5723,14 @@ void theory_seq::add_at_axiom(expr* e) {
expr_ref_vector es(m);
expr_ref nth(m);
unsigned k = iv.get_unsigned();
if (k > m_max_unfolding_depth && m_max_unfolding_lit != null_literal) {
add_axiom(~m_max_unfolding_lit, i_ge_len_s);
}
else {
for (unsigned j = 0; j <= k; ++j) {
es.push_back(m_util.str.mk_unit(mk_nth(s, m_autil.mk_int(j))));
ensure_enode(es.back());
}
nth = es.back();
es.push_back(mk_skolem(m_tail, s, i));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, m_util.str.mk_concat(es)));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e));
for (unsigned j = 0; j <= k; ++j) {
es.push_back(m_util.str.mk_unit(mk_nth(s, m_autil.mk_int(j))));
ensure_enode(es.back());
}
nth = es.back();
es.push_back(mk_skolem(m_tail, s, i));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, m_util.str.mk_concat(es)));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e));
}
else {
expr_ref x = mk_skolem(m_pre, s, i);
@ -5775,6 +5770,7 @@ void theory_seq::add_nth_axiom(expr* e) {
expr_ref rhs(s, m);
expr_ref lhs(m_util.str.mk_unit(e), m);
if (!m_util.str.is_at(s) || zero != i) rhs = m_util.str.mk_at(s, i);
m_rewrite(rhs);
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(lhs, rhs, false));
}
}