mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix regression from #2061 breaking #2074

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-07 16:30:04 -08:00
parent 14f3ff0b63
commit b63a0e31d3
3 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -459,9 +459,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_SEQ_AT:
SASSERT(num_args == 2);
return mk_seq_at(args[0], args[1], result);
#if 0
case OP_SEQ_NTH:
SASSERT(num_args == 2);
return mk_seq_nth(args[0], args[1], result);
#endif
case OP_SEQ_PREFIX:
SASSERT(num_args == 2);
return mk_seq_prefix(args[0], args[1], result);
@ -896,15 +898,9 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
if (m_util.str.is_unit(a, u)) {
if (len == i) {
result = u;
return BR_REWRITE1;
return BR_DONE;
}
}
else if (i > 0) {
SASSERT(len >= i);
result = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
result = m().mk_app(m_util.get_family_id(), OP_SEQ_NTH, result, m_autil.mk_int(len - i));
return BR_REWRITE2;
}
else {
return BR_FAILED;
}

15
src/smt/theory_seq.cpp
View file

@ -4261,6 +4261,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_at(n)) {
add_at_axiom(n);
}
else if (m_util.str.is_nth(n)) {
add_nth_axiom(n);
}
else if (m_util.str.is_string(n)) {
add_elim_string_axiom(n);
}
@ -4965,6 +4968,17 @@ void theory_seq::add_at_axiom(expr* e) {
add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
}
void theory_seq::add_nth_axiom(expr* e) {
expr* s = nullptr, *i = nullptr;
rational n;
zstring str;
VERIFY(m_util.str.is_nth(e, s, i));
if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) {
app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
add_axiom(mk_eq(ch, e, false));
}
}
/*
lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
@ -5431,6 +5445,7 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
m_util.str.is_nth(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_string(n) ||
m_util.str.is_itos(n) ||

1
src/smt/theory_seq.h
View file

@ -575,6 +575,7 @@ namespace smt {
expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_nth_axiom(expr* n);
void add_in_re_axiom(expr* n);
void add_itos_axiom(expr* n);
void add_stoi_axiom(expr* n);