From 0ef0ed3b9461ac43683b9c6233d58da29f8be902 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Dec 2021 15:51:52 -0800 Subject: [PATCH] redoing arrays --- src/sat/smt/array_axioms.cpp | 3 ++- src/sat/smt/array_internalize.cpp | 36 ++++++++++++-------------- src/sat/smt/array_solver.cpp | 16 ++++++------ src/sat/smt/array_solver.h | 7 +++--- src/sat/smt/euf_solver.cpp | 7 ++---- src/sat/smt/smt_relevant.cpp | 42 +++++++++++++++++++++---------- src/sat/smt/smt_relevant.h | 2 +- 7 files changed, 61 insertions(+), 52 deletions(-) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 6f823aee7..6e0310bdd 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -517,13 +517,14 @@ namespace array { unsigned num_vars = get_num_vars(); bool change = false; for (unsigned v = 0; v < num_vars; v++) { - propagate_parent_select_axioms(v); auto& d = get_var_data(v); if (!d.m_prop_upward) continue; euf::enode* n = var2enode(v); if (!ctx.is_relevant(n)) continue; + for (euf::enode* lambda : d.m_parent_lambdas) + propagate_select_axioms(d, lambda); if (add_as_array_eqs(n)) change = true; bool has_default = false; diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index da129f30f..e45d59bd9 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -49,7 +49,7 @@ namespace array { if (v == euf::null_theory_var) { mk_var(n); if (is_lambda(n->get_expr())) - internalize_eh_lambda(n); + internalize_lambda_eh(n); } } @@ -91,18 +91,13 @@ namespace array { return true; } - void solver::internalize_eh_lambda(euf::enode* n) { - SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_map(n->get_expr()) || a.is_as_array(n->get_expr())); - theory_var v = n->get_th_var(get_id()); + void solver::internalize_lambda_eh(euf::enode* n) { push_axiom(default_axiom(n)); - add_lambda(v, n); + auto& d = get_var_data(find(n)); + ctx.push_vec(d.m_lambdas, n); } void solver::internalize_eh(euf::enode* n) { - if (is_lambda(n->get_expr())) { - internalize_eh_lambda(n); - return; - } switch (n->get_decl()->get_decl_kind()) { case OP_STORE: push_axiom(store_axiom(n)); @@ -111,20 +106,19 @@ namespace array { break; case OP_AS_ARRAY: case OP_CONST_ARRAY: - internalize_eh_lambda(n); - // SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward); + internalize_lambda_eh(n); break; case OP_ARRAY_EXT: SASSERT(is_array(n->get_arg(0))); push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1))); break; case OP_ARRAY_DEFAULT: - add_parent_default(n->get_arg(0)->get_th_var(get_id()), n); + add_parent_default(find(n->get_arg(0)), n); break; case OP_ARRAY_MAP: for (auto* arg : euf::enode_args(n)) - add_parent_lambda(arg->get_th_var(get_id()), n); - internalize_eh_lambda(n); + add_parent_lambda(find(arg), n); + internalize_lambda_eh(n); break; case OP_SET_UNION: case OP_SET_INTERSECT: @@ -143,7 +137,7 @@ namespace array { void solver::relevant_eh(euf::enode* n) { if (is_lambda(n->get_expr())) { - set_prop_upward(n->get_th_var(get_id())); + set_prop_upward(find(n)); return; } if (!is_app(n->get_expr())) @@ -152,23 +146,25 @@ namespace array { return; switch (n->get_decl()->get_decl_kind()) { case OP_STORE: - add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n); + add_parent_lambda(find(n->get_arg(0)), n); break; case OP_SELECT: - add_parent_select(n->get_arg(0)->get_th_var(get_id()), n); + add_parent_select(find(n->get_arg(0)), n); break; - case OP_AS_ARRAY: case OP_CONST_ARRAY: - set_prop_upward(n->get_th_var(get_id())); + case OP_AS_ARRAY: + set_prop_upward(find(n)); + add_parent_default(find(n), n); break; case OP_ARRAY_EXT: break; case OP_ARRAY_DEFAULT: - set_prop_upward(n->get_arg(0)->get_th_var(get_id())); + set_prop_upward(find(n->get_arg(0))); break; case OP_ARRAY_MAP: for (auto* arg : euf::enode_args(n)) set_prop_upward_store(arg); + set_prop_upward(find(n)); break; case OP_SET_UNION: case OP_SET_INTERSECT: diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 83fa15f41..f3414a4c6 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -186,18 +186,17 @@ namespace array { if (should_set_prop_upward(d)) set_prop_upward(d); ctx.push_vec(d.m_lambdas, lambda); - if (should_set_prop_upward(d)) { - set_prop_upward_store(lambda); - propagate_select_axioms(d, lambda); - } + propagate_select_axioms(d, lambda); + if (should_set_prop_upward(d)) + set_prop_upward_store(lambda); } void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) { SASSERT(can_beta_reduce(lambda)); auto& d = get_var_data(find(v_child)); ctx.push_vec(d.m_parent_lambdas, lambda); -// if (should_set_prop_upward(d)) -// propagate_select_axioms(d, lambda); + if (should_prop_upward(d)) + propagate_select_axioms(d, lambda); } void solver::add_parent_default(theory_var v, euf::enode* def) { @@ -227,12 +226,13 @@ namespace array { return; auto& d = get_var_data(v); - if (!d.m_prop_upward) - return; for (euf::enode* lambda : d.m_lambdas) propagate_select_axioms(d, lambda); + if (!should_prop_upward(d)) + return; + for (euf::enode* lambda : d.m_parent_lambdas) propagate_select_axioms(d, lambda); } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index b4fd0d95e..1e596bec1 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -66,6 +66,7 @@ namespace array { array_union_find m_find; theory_var find(theory_var v) { return m_find.find(v); } + theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); } func_decl_ref_vector const& sort2diff(sort* s); // internalize @@ -73,8 +74,8 @@ namespace array { bool visited(expr* e) override; bool post_visit(expr* e, bool sign, bool root) override; void ensure_var(euf::enode* n); - void internalize_eh_lambda(euf::enode* n); void internalize_eh(euf::enode* n); + void internalize_lambda_eh(euf::enode* n); // axioms struct axiom_record { @@ -192,7 +193,7 @@ namespace array { // solving void add_parent_select(theory_var v_child, euf::enode* select); void add_parent_default(theory_var v_child, euf::enode* def); - void add_lambda(theory_var v, euf::enode* lambda); + void add_lambda(theory_var v, euf::enode* lambda); void add_parent_lambda(theory_var v_child, euf::enode* lambda); void propagate_select_axioms(var_data const& d, euf::enode* a); @@ -227,8 +228,6 @@ namespace array { void set_else(theory_var v, expr* e); expr* get_else(theory_var v); - void internalized(euf::enode* n); - // diagnostics std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const; std::ostream& display(std::ostream& out, axiom_record const& r) const; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 8f7c34719..eeb195429 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -298,12 +298,9 @@ namespace euf { void solver::asserted(literal l) { if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) { - if (s().lvl(l) <= s().search_lvl()) - mark_relevant(l); - else { - m_relevancy.asserted(l); + m_relevancy.asserted(l); + if (!m_relevancy.is_relevant(l)) return; - } } expr* e = m_bool_var2expr.get(l.var(), nullptr); diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/smt_relevant.cpp index 1f57dc20a..a037090a2 100644 --- a/src/sat/smt/smt_relevant.cpp +++ b/src/sat/smt/smt_relevant.cpp @@ -241,19 +241,35 @@ namespace smt { } void relevancy::propagate_relevant(euf::enode* n) { - m_stack.push_back(n); - while (!m_stack.empty()) { - n = m_stack.back(); - unsigned sz = m_stack.size(); - for (euf::enode* arg : euf::enode_args(n)) - if (!arg->is_relevant()) - m_stack.push_back(arg); - if (sz == m_stack.size()) { - ctx.get_egraph().set_relevant(n); - relevant_eh(n); - for (euf::enode* sib : euf::enode_class(n)) - if (!sib->is_relevant()) - mark_relevant(sib); + m_todo.push_back(n); + while (!m_todo.empty()) { + n = m_todo.back(); + m_todo.pop_back(); + if (n->is_relevant()) + continue; + if (ctx.get_si().is_bool_op(n->get_expr())) + continue; + m_stack.push_back(n); + while (!m_stack.empty()) { + n = m_stack.back(); + unsigned sz = m_stack.size(); + for (euf::enode* arg : euf::enode_args(n)) + if (!arg->is_relevant()) + m_stack.push_back(arg); + if (sz != m_stack.size()) + continue; + if (!n->is_relevant()) { + ctx.get_egraph().set_relevant(n); + relevant_eh(n); + for (euf::enode* sib : euf::enode_class(n)) + if (!sib->is_relevant()) + m_todo.push_back(sib); + } + if (!ctx.get_manager().inc()) { + m_todo.reset(); + m_stack.reset(); + return; + } m_stack.pop_back(); } } diff --git a/src/sat/smt/smt_relevant.h b/src/sat/smt/smt_relevant.h index fbef05b78..723cf613a 100644 --- a/src/sat/smt/smt_relevant.h +++ b/src/sat/smt/smt_relevant.h @@ -119,7 +119,7 @@ namespace smt { vector m_occurs; // where do literals occur unsigned m_qhead = 0; // queue head for relevancy svector> m_queue; // propagation queue for relevancy - euf::enode_vector m_stack; + euf::enode_vector m_stack, m_todo; // callbacks during propagation void relevant_eh(euf::enode* n);