From c44c8284bd21472d66dc04c56cc99b83bb10e88e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jun 2017 18:10:36 -0700 Subject: [PATCH] use worklist algorithm to avoid stack overflow #1125 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 116 ++++++++++++++++++++++++++++------------- src/smt/theory_seq.h | 3 ++ 2 files changed, 83 insertions(+), 36 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4dfff21c2..1c293ad8d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2863,77 +2863,121 @@ bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, de return change; } - -expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { +expr_ref theory_seq::expand(expr* e, dependency*& eqs) { + unsigned sz = m_expand_todo.size(); + m_expand_todo.push_back(e); + expr_ref result(m); + while (m_expand_todo.size() != sz) { + expr* e = m_expand_todo.back(); + result = expand1(e, eqs); + if (result.get()) m_expand_todo.pop_back(); + } + return result; +} + +expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref result(m); - dependency* deps = 0; expr_dep ed; - if (m_rep.find_cache(e0, ed)) { + if (m_rep.find_cache(e, ed)) { eqs = m_dm.mk_join(eqs, ed.second); result = ed.first; - return result; } + else { + m_expand_todo.push_back(e); + } + return result; +} +expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { + expr_ref result(m); + dependency* deps = 0; + result = try_expand(e0, deps); + if (result) return result; expr* e = m_rep.find(e0, deps); expr* e1, *e2, *e3; + expr_ref arg1(m), arg2(m); context& ctx = get_context(); if (m_util.str.is_concat(e, e1, e2)) { - result = mk_concat(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = mk_concat(arg1, arg2); } else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { result = e; } else if (m_util.str.is_prefix(e, e1, e2)) { - result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_prefix(arg1, arg2); } else if (m_util.str.is_suffix(e, e1, e2)) { - result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_suffix(arg1, arg2); } else if (m_util.str.is_contains(e, e1, e2)) { - result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_contains(arg1, arg2); } else if (m_util.str.is_unit(e, e1)) { - result = m_util.str.mk_unit(expand(e1, deps)); + arg1 = try_expand(e1, deps); + if (!arg1) return result; + result = m_util.str.mk_unit(arg1); } else if (m_util.str.is_index(e, e1, e2)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, m_autil.mk_int(0)); } else if (m_util.str.is_index(e, e1, e2, e3)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, e3); } else if (m.is_ite(e, e1, e2, e3)) { if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e2)->get_root()) { - result = expand(e2, deps); + result = try_expand(e2, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e2)); } else if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e3)->get_root()) { - result = expand(e3, deps); + result = try_expand(e3, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e3)); } else { - literal lit(mk_literal(e1)); + literal lit(mk_literal(e1)); #if 0 - expr_ref sk_ite = mk_sk_ite(e1, e2, e3); - add_axiom(~lit, mk_eq(e2, sk_ite, false)); - add_axiom( lit, mk_eq(e3, sk_ite, false)); - result = sk_ite; - + expr_ref sk_ite = mk_sk_ite(e1, e2, e3); + add_axiom(~lit, mk_eq(e2, sk_ite, false)); + add_axiom( lit, mk_eq(e3, sk_ite, false)); + result = sk_ite; + #else - switch (ctx.get_assignment(lit)) { - case l_true: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); - result = expand(e2, deps); - break; - case l_false: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); - result = expand(e3, deps); - break; - case l_undef: - result = e; - m_reset_cache = true; - TRACE("seq", tout << "undef: " << result << "\n"; - tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); - break; - } + switch (ctx.get_assignment(lit)) { + case l_true: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); + result = try_expand(e2, deps); + if (!result) return result; + break; + case l_false: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); + result = try_expand(e3, deps); + if (!result) return result; + break; + case l_undef: + result = e; + m_reset_cache = true; + TRACE("seq", tout << "undef: " << result << "\n"; + tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); + break; + } #endif } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 5fd31e2ca..f7212e608 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -462,7 +462,10 @@ namespace smt { expr_ref canonize(expr* e, dependency*& eqs); bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs); bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs); + ptr_vector m_expand_todo; expr_ref expand(expr* e, dependency*& eqs); + expr_ref expand1(expr* e, dependency*& eqs); + expr_ref try_expand(expr* e, dependency*& eqs); void add_dependency(dependency*& dep, enode* a, enode* b); void get_concat(expr* e, ptr_vector& concats);