From 566eacd424b356a33b208d120e0cb4f4889b9d5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Nov 2019 21:17:36 -0800 Subject: [PATCH] change handling of weak array mode. Insert weak delay variables into a queue that gets consumed by the next propagation when the array_weak parameter is changed #2686 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array.cpp | 19 ++++++------------- src/smt/theory_array.h | 2 +- src/smt/theory_array_base.cpp | 21 +++++++++++++++++++-- src/smt/theory_array_base.h | 6 +++++- src/smt/theory_array_full.cpp | 32 ++++++++------------------------ 5 files changed, 39 insertions(+), 41 deletions(-) diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 23cc45e54..d80660727 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -104,10 +104,6 @@ namespace smt { for (enode* store : d->m_parent_stores) { SASSERT(is_store(store)); if (!m_params.m_array_cg || store->is_cgr()) { - if (m_params.m_array_weak) { - found_unsupported_op(store->get_owner()); - break; - } instantiate_axiom2b(s, store); } } @@ -125,10 +121,6 @@ namespace smt { if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) { for (enode* n : d->m_parent_selects) { if (!m_params.m_array_cg || n->is_cgr()) { - if (m_params.m_array_weak) { - found_unsupported_op(s); - break; - } instantiate_axiom2b(n, s); } } @@ -152,13 +144,13 @@ namespace smt { v = find(v); var_data * d = m_var_data[v]; if (!d->m_prop_upward) { + if (m_params.m_array_weak) { + add_weak_var(v); + return; + } TRACE("array", tout << "#" << v << "\n";); m_trail_stack.push(reset_flag_trail(d->m_prop_upward)); d->m_prop_upward = true; - if (m_params.m_array_weak) { - found_unsupported_op(v); - return; - } if (!m_params.m_array_delay_exp_axiom) instantiate_axiom2b_for(v); for (enode * n : d->m_stores) @@ -401,7 +393,8 @@ namespace smt { r = assert_delayed_axioms(); } } - if (r == FC_DONE && m_found_unsupported_op && !get_context().get_fparams().m_array_fake_support) + bool should_giveup = m_found_unsupported_op || has_propagate_up_trail(); + if (r == FC_DONE && should_giveup && !get_context().get_fparams().m_array_fake_support) r = FC_GIVEUP; CTRACE("array", r != FC_DONE || m_found_unsupported_op, tout << r << "\n";); return r; diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 33a0a5735..16ef8af0a 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -69,7 +69,7 @@ namespace smt { void reset_eh() override; void init_search_eh() override { m_final_check_idx = 0; } - virtual void set_prop_upward(theory_var v); + void set_prop_upward(theory_var v) override; virtual void set_prop_upward(enode* n); virtual void set_prop_upward(theory_var v, var_data* d); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 1586a9b8c..1c2dbb9ea 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -28,10 +28,16 @@ namespace smt { theory_array_base::theory_array_base(ast_manager & m): theory(m.mk_family_id("array")), - m_found_unsupported_op(false) + m_found_unsupported_op(false), + m_array_weak_head(0) { } + void theory_array_base::add_weak_var(theory_var v) { + get_context().push_trail(push_back_vector>(m_array_weak_trail)); + m_array_weak_trail.push_back(v); + } + void theory_array_base::found_unsupported_op(expr * n) { if (!get_context().get_fparams().m_array_fake_support && !m_found_unsupported_op) { TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";); @@ -404,7 +410,12 @@ namespace smt { } bool theory_array_base::can_propagate() { - return !m_axiom1_todo.empty() || !m_axiom2_todo.empty() || !m_extensionality_todo.empty() || !m_congruent_todo.empty(); + return + !m_axiom1_todo.empty() || + !m_axiom2_todo.empty() || + !m_extensionality_todo.empty() || + !m_congruent_todo.empty() || + (!get_context().get_fparams().m_array_weak && has_propagate_up_trail()); } void theory_array_base::propagate() { @@ -421,6 +432,12 @@ namespace smt { assert_congruent_core(m_congruent_todo[i].first, m_congruent_todo[i].second); m_extensionality_todo.reset(); m_congruent_todo.reset(); + if (!get_context().get_fparams().m_array_weak && has_propagate_up_trail()) { + get_context().push_trail(value_trail(m_array_weak_head)); + for (; m_array_weak_head < m_array_weak_trail.size(); ++m_array_weak_head) { + set_prop_upward(m_array_weak_trail[m_array_weak_head]); + } + } } } diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 0bc61edc8..ec47b9608 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -30,7 +30,11 @@ namespace smt { friend class theory_array_bapa; protected: bool m_found_unsupported_op; - + unsigned m_array_weak_head; + svector m_array_weak_trail; + bool has_propagate_up_trail() const { return m_array_weak_head < m_array_weak_trail.size(); } + void add_weak_var(theory_var v); + virtual void set_prop_upward(theory_var v) {} void found_unsupported_op(expr * n); void found_unsupported_op(enode* n) { found_unsupported_op(n->get_owner()); } void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_owner()); } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 94ed6ea50..15852e8b0 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -91,10 +91,6 @@ namespace smt { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { for (enode * n : d->m_parent_selects) { if (!m_params.m_array_cg || n->is_cgr()) { - if (m_params.m_array_weak) { - found_unsupported_op(s); - break; - } instantiate_select_map_axiom(n, s); } } @@ -108,13 +104,13 @@ namespace smt { v = find(v); var_data * d = m_var_data[v]; if (!d->m_prop_upward) { + if (m_params.m_array_weak) { + add_weak_var(v); + return; + } m_trail_stack.push(reset_flag_trail(d->m_prop_upward)); d->m_prop_upward = true; TRACE("array", tout << "#" << v << "\n";); - if (m_params.m_array_weak) { - found_unsupported_op(v); - return; - } if (!m_params.m_array_delay_exp_axiom) { instantiate_axiom2b_for(v); instantiate_axiom_map_for(v); @@ -364,12 +360,7 @@ namespace smt { } if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { - if (m_params.m_array_weak) { - found_unsupported_op(v); - } - else { - instantiate_parent_stores_default(v); - } + instantiate_parent_stores_default(v); } } @@ -393,10 +384,6 @@ namespace smt { for (enode * map : d_full->m_parent_maps) { SASSERT(is_map(map)); if (!m_params.m_array_cg || map->is_cgr()) { - if (m_params.m_array_weak) { - found_unsupported_op(s); - break; - } instantiate_select_map_axiom(s, map); } } @@ -757,10 +744,7 @@ namespace smt { if (d->m_prop_upward && instantiate_axiom_map_for(v)) r = FC_CONTINUE; if (d->m_prop_upward) { - if (m_params.m_array_weak) { - found_unsupported_op(v); - } - else if (instantiate_parent_stores_default(v)) + if (instantiate_parent_stores_default(v)) r = FC_CONTINUE; } } @@ -775,8 +759,8 @@ namespace smt { if (r == FC_DONE && m_bapa) { r = m_bapa->final_check(); } - - if (r == FC_DONE && m_found_unsupported_op) + bool should_giveup = m_found_unsupported_op || has_propagate_up_trail(); + if (r == FC_DONE && should_giveup) r = FC_GIVEUP; return r; }