From 0a29002c2f551504f80a25071d28c5cb8042e88e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Aug 2019 00:20:41 +0800 Subject: [PATCH] return unknown if m_array_weak was used and result is satisfiable Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 10 +++++++++ src/smt/theory_array.cpp | 27 +++++++++++++++++------- src/smt/theory_array_base.h | 2 ++ src/smt/theory_array_full.cpp | 34 +++++++++++++++++++++++-------- src/smt/theory_seq.cpp | 2 +- src/util/params.cpp | 4 ++-- 6 files changed, 61 insertions(+), 18 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e6a233d3c..d61af5057 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -954,6 +954,16 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } unsigned len = r.get_unsigned(); + expr* a2 = nullptr, *i2 = nullptr; + if (m_util.str.is_at(a, a2, i2)) { + if (len > 0) { + result = m_util.str.mk_empty(m().get_sort(a)); + } + else { + result = a2; + } + return BR_DONE; + } expr_ref_vector as(m()); m_util.str.get_concat_units(a, as); diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index f3420df45..c1d6cac27 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -100,10 +100,14 @@ namespace smt { for (enode* n : d->m_stores) { instantiate_axiom2a(s, n); } - if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { + if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { 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); } } @@ -118,10 +122,17 @@ namespace smt { var_data * d = m_var_data[v]; d->m_parent_stores.push_back(s); m_trail_stack.push(push_back_trail(d->m_parent_stores)); - if (!m_params.m_array_weak && !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 (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); + } + } + } } bool theory_array::instantiate_axiom2b_for(theory_var v) { @@ -138,15 +149,17 @@ namespace smt { \brief Mark v for upward propagation. That is, enables the propagation of select(v, i) to store(v,j,k). */ void theory_array::set_prop_upward(theory_var v) { - if (m_params.m_array_weak) - return; v = find(v); var_data * d = m_var_data[v]; if (!d->m_prop_upward) { 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_delay_exp_axiom) + 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) set_prop_upward(n); diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 75de7d7e9..d6b02c9a7 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -32,6 +32,8 @@ namespace smt { bool m_found_unsupported_op; 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()); } bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); } bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 156a9aefb..2a583f16e 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -87,9 +87,13 @@ namespace smt { var_data_full * d_full = m_var_data_full[v]; d_full->m_parent_maps.push_back(s); m_trail_stack.push(push_back_trail(d_full->m_parent_maps)); - if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { + 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); } } @@ -100,14 +104,16 @@ namespace smt { // set set_prop_upward on root and recursively on children if necessary. // void theory_array_full::set_prop_upward(theory_var v) { - if (m_params.m_array_weak) - return; v = find(v); var_data * d = m_var_data[v]; if (!d->m_prop_upward) { 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); @@ -355,8 +361,13 @@ namespace smt { instantiate_default_store_axiom(store); } - if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { - instantiate_parent_stores_default(v); + 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); + } } } @@ -376,10 +387,14 @@ namespace smt { SASSERT(is_map(map)); instantiate_select_map_axiom(s, map); } - if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { + if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { 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); } } @@ -748,8 +763,11 @@ namespace smt { var_data * d = m_var_data[v]; if (d->m_prop_upward && instantiate_axiom_map_for(v)) r = FC_CONTINUE; - if (d->m_prop_upward && !m_params.m_array_weak) { - if (instantiate_parent_stores_default(v)) + if (d->m_prop_upward) { + if (m_params.m_array_weak) { + found_unsupported_op(v); + } + else if (instantiate_parent_stores_default(v)) r = FC_CONTINUE; } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cdf2dad3c..25c51af1a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5208,7 +5208,7 @@ void theory_seq::add_nth_axiom(expr* e) { expr_ref zero(m_autil.mk_int(0), m); literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero)); literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero)); - add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false)); + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false)); } } diff --git a/src/util/params.cpp b/src/util/params.cpp index d91c08bca..82376e965 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -324,8 +324,8 @@ class params { }; }; typedef std::pair entry; - svector m_entries; - std::atomic m_ref_count; + svector m_entries; + std::atomic m_ref_count; void del_value(entry & e); void del_values();