From 7585f28dec4e460cee54665585b25cd02bfbf532 Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Sun, 8 Apr 2018 18:16:38 +0200 Subject: [PATCH] Improved quantifier instantiation logging --- src/smt/mam.cpp | 27 ++++++------ src/smt/mam.h | 3 +- src/smt/smt_context.cpp | 5 ++- src/smt/smt_context.h | 3 +- src/smt/smt_enode.cpp | 1 + src/smt/smt_enode.h | 6 +++ src/smt/smt_model_checker.cpp | 3 +- src/smt/smt_quantifier.cpp | 78 ++++++++++++++++++++++++++++++++--- src/smt/smt_quantifier.h | 3 +- src/smt/smt_quick_checker.cpp | 3 +- 10 files changed, 108 insertions(+), 24 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 5c881684f..acd21f9a2 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1866,7 +1866,7 @@ namespace smt { enode * m_n2; enode * m_app; const bind * m_b; - ptr_vector m_used_enodes; + vector> m_used_enodes; unsigned m_curr_used_enodes_size; ptr_vector m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation unsigned_vector m_min_top_generation, m_max_top_generation; @@ -1883,11 +1883,11 @@ namespace smt { m_pool.recycle(v); } - void update_max_generation(enode * n) { + void update_max_generation(enode * n, enode * prev) { m_max_generation = std::max(m_max_generation, n->get_generation()); if (m_ast_manager.has_trace_stream()) - m_used_enodes.push_back(n); + m_used_enodes.push_back(std::make_tuple(prev, n)); } // We have to provide the number of expected arguments because we have flat-assoc applications such as +. @@ -1896,7 +1896,7 @@ namespace smt { enode * first = curr; do { if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { - update_max_generation(curr); + update_max_generation(curr, first); return curr; } curr = curr->get_next(); @@ -1909,7 +1909,7 @@ namespace smt { curr = curr->get_next(); while (curr != first) { if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { - update_max_generation(curr); + update_max_generation(curr, first); return curr; } curr = curr->get_next(); @@ -1933,7 +1933,7 @@ namespace smt { do { if (n->get_decl() == f && n->get_arg(0)->get_root() == m_args[0]) { - update_max_generation(n); + update_max_generation(n, first); return true; } n = n->get_next(); @@ -1948,7 +1948,7 @@ namespace smt { if (n->get_decl() == f && n->get_arg(0)->get_root() == m_args[0] && n->get_arg(1)->get_root() == m_args[1]) { - update_max_generation(n); + update_max_generation(n, first); return true; } n = n->get_next(); @@ -1968,7 +1968,7 @@ namespace smt { break; } if (i == num_args) { - update_max_generation(n); + update_max_generation(n, first); return true; } } @@ -2213,7 +2213,7 @@ namespace smt { if (bp.m_it == bp.m_end) return nullptr; m_top++; - update_max_generation(*(bp.m_it)); + update_max_generation(*(bp.m_it), nullptr); return *(bp.m_it); } @@ -2294,7 +2294,7 @@ namespace smt { if (m_ast_manager.has_trace_stream()) { m_used_enodes.reset(); - m_used_enodes.push_back(n); + m_used_enodes.push_back(std::make_tuple(nullptr, n)); } m_pc = t->get_root(); @@ -2399,6 +2399,9 @@ namespace smt { SASSERT(m_n2 != 0); if (m_n1->get_root() != m_n2->get_root()) goto backtrack; + + m_used_enodes.push_back(std::make_tuple(m_n1, m_n2)); + m_pc = m_pc->m_next; goto main_loop; @@ -2793,7 +2796,7 @@ namespace smt { m_pattern_instances.pop_back(); m_pattern_instances.push_back(m_app); // continue succeeded - update_max_generation(m_app); + update_max_generation(m_app, nullptr); TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); m_num_args = c->m_num_args; m_oreg = c->m_oreg; @@ -3932,7 +3935,7 @@ namespace smt { } #endif - void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector & used_enodes) override { + void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector> & used_enodes) override { TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); #ifdef Z3DEBUG if (m_check_missing_instances) { diff --git a/src/smt/mam.h b/src/smt/mam.h index 635cb30e7..f6b2958c5 100644 --- a/src/smt/mam.h +++ b/src/smt/mam.h @@ -21,6 +21,7 @@ Revision History: #include "ast/ast.h" #include "smt/smt_types.h" +#include namespace smt { /** @@ -57,7 +58,7 @@ namespace smt { virtual void display(std::ostream& out) = 0; - virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector & used_enodes) = 0; + virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector> & used_enodes) = 0; virtual bool is_shared(enode * n) const = 0; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index dd38776bc..8a37ba61e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -558,6 +558,7 @@ namespace smt { invert_trans(n1); n1->m_trans.m_target = n2; n1->m_trans.m_justification = js; + n1->m_proof_is_logged = false; SASSERT(r1->trans_reaches(n1)); // --------------- // r1 -> .. -> n1 -> n2 -> ... -> r2 @@ -749,6 +750,7 @@ namespace smt { eq_justification new_js = curr->m_trans.m_justification; curr->m_trans.m_target = prev; curr->m_trans.m_justification = js; + curr->m_proof_is_logged = false; prev = curr; js = new_js; curr = new_curr; @@ -1045,6 +1047,7 @@ namespace smt { SASSERT(r1->trans_reaches(n1)); n1->m_trans.m_target = nullptr; n1->m_trans.m_justification = null_eq_justification; + n1->m_proof_is_logged = false; invert_trans(r1); // --------------- // n1 -> ... -> r1 @@ -1809,7 +1812,7 @@ namespace smt { } bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, - unsigned min_top_generation, unsigned max_top_generation, ptr_vector & used_enodes) { + unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes) { return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index a4581b020..f4e7b72e0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -49,6 +49,7 @@ Revision History: #include "util/timer.h" #include "util/statistics.h" #include "solver/progress_callback.h" +#include // there is a significant space overhead with allocating 1000+ contexts in // the case that each context only references a few expressions. @@ -946,7 +947,7 @@ namespace smt { bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings); bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, - unsigned min_top_generation, unsigned max_top_generation, ptr_vector & used_enodes); + unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes); void set_global_generation(unsigned generation) { m_generation = generation; } diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index e09e83f6b..d14c37906 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -47,6 +47,7 @@ namespace smt { n->m_cgc_enabled = cgc_enabled; n->m_iscope_lvl = iscope_lvl; n->m_lbl_hash = -1; + n->m_proof_is_logged = false; unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; i++) { enode * arg = app2enode[owner->get_arg(i)->get_id()]; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index b216665e5..d4aebd56b 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -105,6 +105,7 @@ namespace smt { enode_vector m_parents; //!< Parent enodes of the equivalence class. theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode. trans_justification m_trans; //!< A justification for the enode being equal to its root. + bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log. signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; @@ -113,6 +114,7 @@ namespace smt { friend class context; friend class euf_manager; friend class conflict_resolution; + friend class quantifier_manager; theory_var_list * get_th_var_list() { @@ -317,6 +319,10 @@ namespace smt { theory_var get_th_var(theory_id th_id) const; + trans_justification get_trans_justification() { + return m_trans; + } + unsigned get_generation() const { return m_generation; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 765cc87f5..549c15148 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -26,6 +26,7 @@ Revision History: #include "smt/smt_context.h" #include "smt/smt_model_finder.h" #include "model/model_pp.h" +#include namespace smt { @@ -476,7 +477,7 @@ namespace smt { void model_checker::assert_new_instances() { TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";); ptr_buffer bindings; - ptr_vector dummy; + vector> dummy; for (instance* inst : m_new_instances) { quantifier * q = inst->m_q; if (m_context->b_internalized(q)) { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 0ca244185..19fe2c14a 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -104,13 +104,64 @@ namespace smt { return m_plugin->is_shared(n); } + inline void log_transitive_justification(std::ostream & log, enode *en) { + enode *root = en->get_root(); + for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { + if (!it->m_proof_is_logged) { + it->m_proof_is_logged = true; + print_justification(log, it); + } + } + if (!root->m_proof_is_logged) { + root->m_proof_is_logged = true; + log << "[eq-expl] #" << root->get_owner_id() << " root\n"; + } + } + + inline void print_justification(std::ostream & out, enode *en) { + smt::literal lit; + unsigned num_args; + enode *target = en->get_trans_justification().m_target; + + switch (en->get_trans_justification().m_justification.get_kind()) { + case smt::eq_justification::kind::EQUATION: + lit = en->get_trans_justification().m_justification.get_literal(); + out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n"; + break; + case smt::eq_justification::kind::AXIOM: + out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n"; + break; + case smt::eq_justification::kind::CONGRUENCE: + if (!en->get_trans_justification().m_justification.used_commutativity()) { + num_args = en->get_num_args(); + + for (unsigned i = 0; i < num_args; i++) { + + log_transitive_justification(out, en->get_arg(i)); + log_transitive_justification(out, target->get_arg(i)); + } + + out << "[eq-expl] #" << en->get_owner_id() << " cg"; + for (unsigned i = 0; i < num_args; i++) { + out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")"; + } + out << " ; #" << target->get_owner_id() << "\n"; + + break; + } + default: + out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n"; + break; + } + } + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, - ptr_vector & used_enodes) { + vector> & used_enodes) { max_generation = std::max(max_generation, get_generation(q)); if (m_num_instances > m_params.m_qi_max_instances) { return false; @@ -120,15 +171,30 @@ namespace smt { if (f) { if (has_trace_stream()) { std::ostream & out = trace_stream(); - out << "[new-match] " << static_cast(f) << " #" << q->get_id(); + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + log_transitive_justification(out, orig); + log_transitive_justification(out, substituted); + } + } + out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); for (unsigned i = 0; i < num_bindings; i++) { // I don't want to use mk_pp because it creates expressions for pretty printing. // This nasty side-effect may change the behavior of Z3. out << " #" << bindings[i]->get_owner_id(); } out << " ;"; - for (enode* n : used_enodes) - out << " #" << n->get_owner_id(); + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) + out << " #" << substituted->get_owner_id(); + else { + out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + } + } out << "\n"; } m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO @@ -294,12 +360,12 @@ namespace smt { unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, - ptr_vector & used_enodes) { + vector> & used_enodes) { return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes); } bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) { - ptr_vector tmp; + vector> tmp; return add_instance(q, nullptr, num_bindings, bindings, generation, generation, generation, tmp); } diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index ad5f58e49..1b1c3547e 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -23,6 +23,7 @@ Revision History: #include "util/statistics.h" #include "util/params.h" #include "smt/smt_types.h" +#include class proto_model; struct smt_params; @@ -57,7 +58,7 @@ namespace smt { unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, - ptr_vector & used_enodes); + vector> & used_enodes); bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0); void init_search_eh(); diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index 64c791a0e..ab75d2dea 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/src/smt/smt_quick_checker.cpp @@ -19,6 +19,7 @@ Revision History: #include "smt/smt_context.h" #include "smt/smt_quick_checker.h" #include "ast/ast_pp.h" +#include namespace smt { @@ -211,7 +212,7 @@ namespace smt { } bool quick_checker::process_candidates(quantifier * q, bool unsat) { - ptr_vector empty_used_enodes; + vector> empty_used_enodes; buffer szs; buffer it; for (unsigned i = 0; i < m_num_bindings; i++) {