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

selective expansion of strings for canonizer to fix #1690 regression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-18 20:37:39 -07:00
parent 8040eddf65
commit 4634d1daed
2 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_seq.cpp
View file

@ -2251,9 +2251,6 @@ bool theory_seq::internalize_term(app* term) {
e = ctx.mk_enode(term, false, m.is_bool(term), true); e = ctx.mk_enode(term, false, m.is_bool(term), true);
} }
mk_var(e); mk_var(e);
if (m_util.str.is_string(term)) {
add_elim_string_axiom(term);
}
return true; return true;
} }
@ -2901,12 +2898,16 @@ expr_ref theory_seq::expand(expr* e, dependency*& eqs) {
expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
expr_ref result(m); expr_ref result(m);
expr_dep ed; expr_dep ed;
zstring s;
if (m_rep.find_cache(e, ed)) { if (m_rep.find_cache(e, ed)) {
if (e != ed.first) { if (e != ed.first) {
eqs = m_dm.mk_join(eqs, ed.second); eqs = m_dm.mk_join(eqs, ed.second);
} }
result = ed.first; result = ed.first;
} }
else if (m_util.str.is_string(e, s) && s.length() > 0) {
result = add_elim_string_axiom(e);
}
else { else {
m_expand_todo.push_back(e); m_expand_todo.push_back(e);
} }
@ -2929,7 +2930,7 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
} }
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
result = e; result = e;
} }
else if (m_util.str.is_prefix(e, e1, e2)) { else if (m_util.str.is_prefix(e, e1, e2)) {
arg1 = try_expand(e1, deps); arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps); arg2 = try_expand(e2, deps);
@ -3286,12 +3287,12 @@ void theory_seq::add_replace_axiom(expr* r) {
tightest_prefix(s, x); tightest_prefix(s, x);
} }
void theory_seq::add_elim_string_axiom(expr* n) { expr_ref theory_seq::add_elim_string_axiom(expr* n) {
zstring s; zstring s;
TRACE("seq", tout << mk_pp(n, m) << "\n";); TRACE("seq", tout << mk_pp(n, m) << "\n";);
VERIFY(m_util.str.is_string(n, s)); VERIFY(m_util.str.is_string(n, s));
if (s.length() == 0) { if (s.length() == 0) {
return; return expr_ref(n, m);
} }
expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m); expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m);
for (unsigned i = s.length()-1; i-- > 0; ) { for (unsigned i = s.length()-1; i-- > 0; ) {
@ -3300,6 +3301,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
add_axiom(mk_eq(n, result, false)); add_axiom(mk_eq(n, result, false));
m_rep.update(n, result, nullptr); m_rep.update(n, result, nullptr);
m_new_solution = true; m_new_solution = true;
return result;
} }

2
src/smt/theory_seq.h
View file

@ -504,7 +504,7 @@ namespace smt {
void add_int_string(expr* e); void add_int_string(expr* e);
bool check_int_string(); bool check_int_string();
void add_elim_string_axiom(expr* n); expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n); void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n); void add_in_re_axiom(expr* n);
void add_itos_axiom(expr* n); void add_itos_axiom(expr* n);