From fce286db918d2568a571b485d44a40d80d865fa0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Jan 2016 17:11:12 -0800 Subject: [PATCH] Issue #354. Fix unsoundness in Array theory based on missing propagation of selects over ite expressions Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/proto_model.cpp | 11 ++++++-- src/smt/proto_model/proto_model.h | 3 ++- src/smt/smt_context.cpp | 1 + src/smt/smt_context.h | 2 ++ src/smt/smt_context_inv.cpp | 39 +++++++++++++++++++++++++++ src/smt/smt_context_pp.cpp | 1 + src/smt/smt_model_checker.cpp | 10 ++++++- src/smt/smt_model_finder.cpp | 2 +- src/smt/theory_array.cpp | 41 +++++++++++++++++++++++++---- src/smt/theory_array_base.cpp | 12 +++++++++ 10 files changed, 112 insertions(+), 10 deletions(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 26ff0136c..024de9f15 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -174,6 +174,13 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu return true; } +bool proto_model::is_select_of_model_value(expr* e) const { + return + is_app_of(e, m_afid, OP_SELECT) && + is_as_array(to_app(e)->get_arg(0)) && + has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); +} + /** \brief Evaluate the expression e in the current model, and store the result in \c result. It returns \c true if succeeded, and false otherwise. If the evaluation fails, @@ -257,7 +264,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); trail.push_back(new_t); - if (!is_app(new_t) || to_app(new_t)->get_decl() != f) { + if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) { // if the result is not of the form (f ...), then assume we must simplify it. expr * new_new_t = 0; if (!eval_cache.find(new_t.get(), new_new_t)) { @@ -588,7 +595,7 @@ void proto_model::register_value(expr * n) { } } -bool proto_model::is_array_value(expr * v) const { +bool proto_model::is_as_array(expr * v) const { return is_app_of(v, m_afid, OP_AS_ARRAY); } diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 578880459..d26f4d70d 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -59,6 +59,7 @@ class proto_model : public model_core { void remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s); void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs); + bool is_select_of_model_value(expr* e) const; public: proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref()); @@ -68,7 +69,7 @@ public: bool eval(expr * e, expr_ref & result, bool model_completion = false); - bool is_array_value(expr * v) const; + bool is_as_array(expr * v) const; value_factory * get_factory(family_id fid); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 04b7ce234..9b9fdf841 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4126,6 +4126,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); + SASSERT(validate_model()); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fd1049626..38463abe2 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1415,6 +1415,8 @@ namespace smt { bool update_model(bool refinalize); void get_proto_model(proto_model_ref & m) const; + + bool validate_model(); unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index dabeab401..50814b686 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -399,6 +399,45 @@ namespace smt { #endif + bool context::validate_model() { + if (!m_proto_model) { + return true; + } + ast_manager& m = m_manager; + literal_vector::const_iterator it = m_assigned_literals.begin(); + literal_vector::const_iterator end = m_assigned_literals.end(); + for (; it != end; ++it) { + literal lit = *it; + if (!is_relevant(lit)) { + continue; + } + expr_ref n(m), res(m); + literal2expr(lit, n); + if (!is_ground(n)) { + continue; + } + switch (get_assignment(*it)) { + case l_undef: + break; + case l_true: + m_proto_model->eval(n, res, false); + CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); + if (m.is_false(res)) { + return false; + } + break; + case l_false: + m_proto_model->eval(n, res, false); + CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); + if (m.is_true(res)) { + return false; + } + break; + } + } + return true; + } + /** \brief validate unsat core returned by */ diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 79684570e..695c71eea 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -239,6 +239,7 @@ namespace smt { first = false; } out << "#" << n->get_id() << " -> #" << r->get_id() << "\n"; + out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n"; } } } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 09b8fe4b6..b294bf4c9 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -346,6 +346,10 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; if(!m_qm->mbqi_enabled(q)) continue; + TRACE("model_checker", + tout << "Check: " << mk_pp(q, m_manager) << "\n"; + tout << m_context->get_assignment(q) << "\n";); + if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; @@ -364,8 +368,12 @@ namespace smt { m_iteration_idx++; TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); - TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); + TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; + + if (num_failures == 0 && !m_context->validate_model()) { + num_failures = 1; + } if (num_failures == 0) m_curr_model->cleanup(); if (m_params.m_mbqi_trace) { diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 2e260cbca..d7dc4d806 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1418,7 +1418,7 @@ namespace smt { func_decl * get_array_func_decl(app * ground_array, auf_solver & s) { expr * ground_array_interp = s.eval(ground_array, false); - if (ground_array_interp != 0 && s.get_model()->is_array_value(ground_array_interp)) + if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp)) return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast()); return 0; } diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 7ba94d9cb..960218dff 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -44,7 +44,9 @@ namespace smt { void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) { // v1 is the new root - TRACE("array", tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1);); + TRACE("array", + tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1); + tout << mk_pp(get_enode(v1)->get_owner(), get_manager()) << " <- " << mk_pp(get_enode(v2)->get_owner(), get_manager()) << "\n";); SASSERT(v1 == find(v1)); var_data * d1 = m_var_data[v1]; var_data * d2 = m_var_data[v2]; @@ -70,21 +72,41 @@ namespace smt { } theory_var theory_array::mk_var(enode * n) { + ast_manager& m = get_manager(); + context& ctx = get_context(); theory_var r = theory_array_base::mk_var(n); theory_var r2 = m_find.mk_var(); SASSERT(r == r2); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; - TRACE("array", tout << mk_bounded_pp(n->get_owner(), get_manager()) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << + TRACE("array", tout << mk_bounded_pp(n->get_owner(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << ", is_store: " << is_store(n) << "\n";); d->m_is_array = is_array_sort(n); if (d->m_is_array) - register_sort(get_manager().get_sort(n->get_owner())); + register_sort(m.get_sort(n->get_owner())); d->m_is_select = is_select(n); + + expr* e1, *e2, *e3; if (is_store(n)) d->m_stores.push_back(n); - get_context().attach_th_var(n, this, r); + else if (m.is_ite(n->get_owner(), e1, e2, e3)) { + ptr_vector todo; + todo.push_back(e2); + todo.push_back(e3); + while (!todo.empty()) { + e1 = todo.back(); + todo.pop_back(); + if (is_app(e1) && is_store(to_app(e1))) { + d->m_stores.push_back(ctx.get_enode(e1)); + } + else if (m.is_ite(e1, e1, e2, e3)) { + todo.push_back(e2); + todo.push_back(e3); + } + } + } + ctx.attach_th_var(n, this, r); if (m_params.m_array_laziness <= 1 && is_store(n)) instantiate_axiom1(n); return r; @@ -97,6 +119,7 @@ namespace smt { v = find(v); var_data * d = m_var_data[v]; d->m_parent_selects.push_back(s); + TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";); m_trail_stack.push(push_back_trail(d->m_parent_selects)); ptr_vector::iterator it = d->m_stores.begin(); ptr_vector::iterator end = d->m_stores.end(); @@ -109,8 +132,13 @@ namespace smt { for (; it != end; ++it) { enode * store = *it; SASSERT(is_store(store)); - if (!m_params.m_array_cg || store->is_cgr()) + std::cout << mk_pp(store->get_owner(), get_manager()) << " " << mk_pp(s->get_owner(), get_manager()) << "\n"; + if (!m_params.m_array_cg || store->is_cgr()) { instantiate_axiom2b(s, store); + } + else { + std::cout << mk_pp(store->get_owner(), get_manager()) << "\n"; + } } } } @@ -331,6 +359,9 @@ namespace smt { void theory_array::relevant_eh(app * n) { if (m_params.m_array_laziness == 0) return; + if (get_manager().is_ite(n)) { + TRACE("array", tout << "relevant ite " << mk_pp(n, get_manager()) << "\n";); + } if (!is_store(n) && !is_select(n)) return; context & ctx = get_context(); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 4526b283a..498f8aeec 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -943,6 +943,18 @@ namespace smt { result->add_entry(args.size(), args.c_ptr(), select); } } + TRACE("array", + tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n"; + if (sel_set) { + select_set::iterator it = sel_set->begin(); + select_set::iterator end = sel_set->end(); + for (; it != end; ++it) { + tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n"; + } + } + if (else_val_n) { + tout << "else: " << mk_pp(else_val_n->get_owner(), get_manager()) << "\n"; + }); return result; }