From 228111511c8293c7a4b35743b141693d4a3b6415 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Mar 2017 18:41:36 +0100 Subject: [PATCH] fixing build break, addressing #935 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + src/smt/mam.cpp | 2 +- src/smt/smt_context.cpp | 40 +++++++++++++++++++++++++++++---- src/smt/smt_context.h | 8 +++++++ src/smt/smt_quantifier.cpp | 26 ++++++++++++++------- 5 files changed, 64 insertions(+), 13 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 67b1df50c..2551f0aa0 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1551,6 +1551,7 @@ void cmd_context::validate_model() { p.set_uint("sort_store", true); p.set_bool("completion", true); model_evaluator evaluator(*(md.get()), p); + evaluator.set_expand_array_equalities(false); contains_array_op_proc contains_array(m()); { scoped_rlimit _rlimit(m().limit(), 0); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 5d03a3563..ba9f970a2 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3942,7 +3942,7 @@ namespace smt { #endif virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector & used_enodes) { - TRACE("trigger_bug", tout << "found match\n";); + TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); #ifdef Z3DEBUG if (m_check_missing_instances) { if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e816f5c73..3fca7d04b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -304,7 +304,6 @@ namespace smt { TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); - SASSERT(l.var() < static_cast(m_b_internalized_stack.size())); m_assigned_literals.push_back(l); m_assignment[l.index()] = l_true; m_assignment[(~l).index()] = l_false; @@ -319,14 +318,23 @@ namespace smt { d.m_phase_available = true; d.m_phase = !l.sign(); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); + TRACE("relevancy", - tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";); - if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var())))) + tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";); + if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l))) m_atom_propagation_queue.push_back(l); if (m_manager.has_trace_stream()) trace_assign(l, j, decision); m_case_split_queue->assign_lit_eh(l); + + // a unit is asserted at search level. Mark it as relevant. + // this addresses bug... where a literal becomes fixed to true (false) + // as a conflict gets assigned misses relevancy (and quantifier instantiation). + // + if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) { + mark_as_relevant(l); + } } bool context::bcp() { @@ -1634,7 +1642,7 @@ namespace smt { m_atom_propagation_queue.push_back(literal(v, val == l_false)); } } - TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << "\n";); + TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";); #ifndef SMTCOMP m_case_split_queue->relevant_eh(n); #endif @@ -3737,7 +3745,9 @@ namespace smt { // I invoke pop_scope_core instead of pop_scope because I don't want // to reset cached generations... I need them to rebuild the literals // of the new conflict clause. + if (relevancy()) record_relevancy(num_lits, lits); unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl); + if (relevancy()) restore_relevancy(num_lits, lits); SASSERT(m_scope_lvl == new_lvl); // the logical context may still be in conflict after // clauses are reinitialized in pop_scope. @@ -3850,6 +3860,28 @@ namespace smt { } return false; } + + /* + \brief we record and restore relevancy information for literals in conflict clauses. + A literal may have been marked relevant within the scope that gets popped during + conflict resolution. In this case, the literal is no longer marked as relevant after + the pop. This can cause quantifier instantiation to miss relevant triggers and thereby + cause incmpleteness. + */ + void context::record_relevancy(unsigned n, literal const* lits) { + m_relevant_conflict_literals.reset(); + for (unsigned i = 0; i < n; ++i) { + m_relevant_conflict_literals.push_back(is_relevant(lits[i])); + } + } + + void context::restore_relevancy(unsigned n, literal const* lits) { + for (unsigned i = 0; i < n; ++i) { + if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) { + mark_as_relevant(lits[i]); + } + } + } void context::get_relevant_labels(expr* cnstr, buffer & result) { if (m_fparams.m_check_at_labels) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index c1c684fec..2a555e6b5 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1103,6 +1103,10 @@ namespace smt { bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); } + svector m_relevant_conflict_literals; + void record_relevancy(unsigned n, literal const* lits); + void restore_relevancy(unsigned n, literal const* lits); + public: // event handler for relevancy_propagator class void relevant_eh(expr * n); @@ -1124,6 +1128,10 @@ namespace smt { return is_relevant(l.var()); } + bool is_relevant_core(literal l) const { + return is_relevant_core(bool_var2expr(l.var())); + } + void mark_as_relevant(expr * n) { m_relevancy_propagator->mark_as_relevant(n); m_relevancy_propagator->propagate(); } void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 2a56168f2..bad788f5d 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -52,8 +52,9 @@ namespace smt { m_qi_queue.setup(); } - bool has_trace_stream() const { return m_context.get_manager().has_trace_stream(); } - std::ostream & trace_stream() { return m_context.get_manager().trace_stream(); } + ast_manager& m() const { return m_context.get_manager(); } + bool has_trace_stream() const { return m().has_trace_stream(); } + std::ostream & trace_stream() { return m().trace_stream(); } quantifier_stat * get_stat(quantifier * q) const { return m_quantifier_stat.find(q); @@ -110,8 +111,9 @@ namespace smt { unsigned max_top_generation, ptr_vector & used_enodes) { max_generation = std::max(max_generation, get_generation(q)); - if (m_num_instances > m_params.m_qi_max_instances) + if (m_num_instances > m_params.m_qi_max_instances) { return false; + } get_stat(q)->update_max_generation(max_generation); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings); if (f) { @@ -132,9 +134,17 @@ namespace smt { } m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; - return true; } - return false; + TRACE("quantifier", + tout << mk_pp(q, m()) << " "; + for (unsigned i = 0; i < num_bindings; ++i) { + tout << mk_pp(bindings[i]->get_owner(), m()) << " "; + } + tout << "\n"; + tout << "inserted: " << (f != 0) << "\n"; + ); + + return f != 0; } void init_search_eh() { @@ -186,7 +196,7 @@ namespace smt { } bool check_quantifier(quantifier* q) { - return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m_context.get_manager().is_rec_fun_def(q); + return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m().is_rec_fun_def(q); } bool quick_check_quantifiers() { @@ -501,13 +511,13 @@ namespace smt { SASSERT(m_context->get_manager().is_pattern(mp)); bool unary = (mp->get_num_args() == 1); if (!unary && j >= num_eager_multi_patterns) { - TRACE("assign_quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n" + TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n" << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";); m_lazy_mam->add_pattern(q, mp); } else { - TRACE("assign_quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";); + TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";); m_mam->add_pattern(q, mp); } if (!unary)