From 3852d4516dbff75a0d00caeffc4f2f400ce7cb90 Mon Sep 17 00:00:00 2001 From: Rocco Salvia Date: Sat, 8 Aug 2020 13:09:24 -0600 Subject: [PATCH] modular Axiom Profiler (#4619) * Rocco first commit * Rocco: clean the log * Rocco: version 0.1 beta of the causality graph * Rocco: minimal fix to separate lines * Rocco: fix the enodes * Rocco: our trace has to reflect same behaviour of the native trace for what concern used_enodes * Rocco: disable trace when dummy instantiations * Rocco: fix to enodes * Update README.md * Rocco: remove causality details and add the pattern (trigger) * Rocco: add ; at the end of the bindings * Rocco: add triggers as separate trace * Rocco README file * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Rocco: bug in tout flush * Update README.md * Update README.md * Rocco: clean code * Ready for pull request * Remove commented line bindings * Add space between // and first char * Substitute or with || for compatibility; Add space around > --- contrib/qprofdiff/Makefile | 0 src/ast/rewriter/rewriter_def.h | 5 +++-- src/ast/rewriter/var_subst.cpp | 11 ++++++++++ src/smt/cached_var_subst.cpp | 8 +++++++ src/smt/mam.cpp | 12 +++++----- src/smt/qi_queue.cpp | 21 +++++++++++++++++- src/smt/smt_internalizer.cpp | 3 ++- src/smt/smt_quantifier.cpp | 39 ++++++++++++++++++++++++++++++++- src/smt/smt_quantifier_stat.cpp | 2 ++ src/smt/smt_quantifier_stat.h | 16 ++++++++++++++ src/util/trace.h | 2 ++ 11 files changed, 108 insertions(+), 11 deletions(-) mode change 100644 => 100755 contrib/qprofdiff/Makefile diff --git a/contrib/qprofdiff/Makefile b/contrib/qprofdiff/Makefile old mode 100644 new mode 100755 diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index b026b6a47..4055161fa 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -654,10 +654,9 @@ void rewriter_tpl::cleanup() { template void rewriter_tpl::display_bindings(std::ostream& out) { - out << "bindings:\n"; for (unsigned i = 0; i < m_bindings.size(); i++) { if (m_bindings[i]) - out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n"; + out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << ";\n"; } } @@ -674,6 +673,7 @@ void rewriter_tpl::set_bindings(unsigned num_bindings, expr * const * bi m_shifts.push_back(num_bindings); } TRACE("rewriter", display_bindings(tout);); + SCTRACE("bindings", is_trace_enabled("coming_from_quant"), display_bindings(tout);); } template @@ -687,6 +687,7 @@ void rewriter_tpl::set_inv_bindings(unsigned num_bindings, expr * const m_shifts.push_back(num_bindings); } TRACE("rewriter", display_bindings(tout);); + SCTRACE("bindings", is_trace_enabled("coming_from_quant"), display_bindings(tout);); } template diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index d833cfd3b..3f70791b9 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -27,6 +27,17 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) expr_ref result(m_reducer.m()); if (is_ground(n)) { result = n; + //application does not have free variables or nested quantifiers. + //There is no need to print the bindings here? + SCTRACE("bindings", is_trace_enabled("coming_from_quant"), + tout << "(ground)\n"; + for (unsigned i = 0; i < num_args; i++) { + if (args[i]) { + tout << i << ": " << mk_ismt2_pp(args[i], result.m()) << ";\n"; + } + } + tout.flush();); + return result; } SASSERT(is_well_sorted(result.m(), n)); diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp index 924630cfb..b2e3cccd1 100644 --- a/src/smt/cached_var_subst.cpp +++ b/src/smt/cached_var_subst.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "smt/cached_var_subst.h" +#include "ast/rewriter/rewriter_def.h" bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cached_var_subst::key * k2) const { if (k1->m_qa != k2->m_qa) @@ -58,6 +59,13 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e // entry was already there m_new_keys[num_bindings] = new_key; // recycle key result = entry->get_data().m_value; + SCTRACE("bindings", is_trace_enabled("coming_from_quant"),tout << "(cache)\n"; + for (unsigned i = 0; i < num_bindings; i++) { + if (new_key->m_bindings[i]) { + tout << i << ": " << mk_ismt2_pp(new_key->m_bindings[i], result.m()) << ";\n"; + } + } + tout.flush();); return; } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index d866bc924..bd4f69486 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1893,7 +1893,7 @@ namespace { void update_max_generation(enode * n, enode * prev) { m_max_generation = std::max(m_max_generation, n->get_generation()); - if (m.has_trace_stream()) + if (m.has_trace_stream() || is_trace_enabled("causality")) m_used_enodes.push_back(std::make_tuple(prev, n)); } @@ -2309,7 +2309,7 @@ namespace { m_pattern_instances.push_back(n); m_max_generation = n->get_generation(); - if (m.has_trace_stream()) { + if (m.has_trace_stream() || is_trace_enabled("causality")) { m_used_enodes.reset(); m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level } @@ -2408,7 +2408,7 @@ namespace { goto backtrack; // We will use the common root when instantiating the quantifier => log the necessary equalities - if (m.has_trace_stream()) { + if (m.has_trace_stream() || is_trace_enabled("causality")) { m_used_enodes.push_back(std::make_tuple(m_n1, m_n1->get_root())); m_used_enodes.push_back(std::make_tuple(m_n2, m_n2->get_root())); } @@ -2425,7 +2425,7 @@ namespace { goto backtrack; // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log - if (m.has_trace_stream()) { + if (m.has_trace_stream() || is_trace_enabled("causality")) { m_used_enodes.push_back(std::make_tuple(m_n1, m_n2)); } @@ -2611,7 +2611,7 @@ namespace { if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \ goto backtrack; \ update_max_generation(m_n1, nullptr); \ - if (m.has_trace_stream()) { \ + if (m.has_trace_stream() || is_trace_enabled("causality")) { \ for (unsigned i = 0; i < static_cast(m_pc)->m_num_args; ++i) { \ m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_n1->get_arg(i)->get_root())); \ } \ @@ -2707,7 +2707,7 @@ namespace { backtrack_point & bp = m_backtrack_stack[m_top - 1]; m_max_generation = bp.m_old_max_generation; - if (m.has_trace_stream()) + if (m.has_trace_stream() || is_trace_enabled("causality")) m_used_enodes.shrink(bp.m_old_used_enodes_size); TRACE("mam_int", tout << "backtrack top: " << bp.m_instr << " " << *(bp.m_instr) << "\n";); diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 98301d6d4..284b469cc 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -202,11 +202,26 @@ namespace smt { ent.m_instantiated = true; TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f << " cost: " << ent.m_cost << "\n";); + // NEVER remove coming_from_quant + // "coming_from_quant" allows the logging of bindings and enodes + // only when they come from instantiations + enable_trace("coming_from_quant"); + quantifier_stat * stat = m_qm.get_stat(q); if (m_checker.is_sat(q->get_expr(), num_bindings, bindings)) { TRACE("checker", tout << "instance already satisfied\n";); + // we log the "dummy" instantiations separately from "instance" + STRACE("dummy", tout << "### " << static_cast(f) <<", " << q->get_qid() << "\n";); + STRACE("dummy", tout << "Instance already satisfied (dummy)\n";); + // a dummy instantiation is still an instantiation. + // in this way smt.qi.profile=true coincides with the axiom profiler + stat->inc_num_instances_checker_sat(); + disable_trace("coming_from_quant"); return; } + + STRACE("instance", tout << "### " << static_cast(f) <<", " << q->get_qid() << "\n";); + expr_ref instance(m); m_subst(q, num_bindings, bindings, instance); @@ -219,15 +234,17 @@ namespace smt { if (m.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m);); + STRACE("instance", tout << "Instance reduced to true\n";); + stat -> inc_num_instances_simplify_true(); if (m.has_trace_stream()) { display_instance_profile(f, q, num_bindings, bindings, pr ? pr->get_id() : 0, generation); m.trace_stream() << "[end-of-instance]\n"; } + disable_trace("coming_from_quant"); return; } TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";); - quantifier_stat * stat = m_qm.get_stat(q); stat->inc_num_instances(); if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) { m_qm.display_stats(verbose_stream(), q); @@ -312,6 +329,8 @@ namespace smt { if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + // NEVER remove coming_from_quant + disable_trace("coming_from_quant"); } void qi_queue::push_scope() { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index a19898452..a90648200 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1011,9 +1011,10 @@ namespace smt { m_stats.m_num_mk_enode++; TRACE("mk_enode", tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n"; if (e->get_num_args() > 0) { - tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: " + tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: " << e->is_cgr() << "\n"; }); + SCTRACE("causality", is_trace_enabled("coming_from_quant"), tout << "EN: #" << e->get_owner_id() << "\n";); if (m.has_trace_stream()) m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n"; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 521a28c01..1853f72ed 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -170,15 +170,21 @@ namespace smt { void display_stats(std::ostream & out, quantifier * q) { quantifier_stat * s = get_stat(q); unsigned num_instances = s->get_num_instances(); + unsigned num_instances_simplify_true = s->get_num_instances_simplify_true(); + unsigned num_instances_checker_sat = s->get_num_instances_checker_sat(); unsigned max_generation = s->get_max_generation(); float max_cost = s->get_max_cost(); - if (num_instances > 0) { + if (num_instances > 0 || num_instances_simplify_true>0 || num_instances_checker_sat>0) { out << "[quantifier_instances] "; out.width(10); out << q->get_qid().str() << " : "; out.width(6); out << num_instances << " : "; out.width(3); + out << num_instances_simplify_true << " : "; + out.width(3); + out << num_instances_checker_sat << " : "; + out.width(3); out << max_generation << " : " << max_cost << "\n"; } } @@ -199,6 +205,33 @@ namespace smt { return m_plugin->is_shared(n); } + void log_causality( + fingerprint* f, + app * pat, + vector> & used_enodes) { + + if (pat != nullptr) { + if (used_enodes.size() > 0) { + STRACE("causality", tout << "New-Match: "<< static_cast(f);); + STRACE("triggers", tout <<", Pat: "<< expr_ref(pat, m());); + STRACE("causality", tout <<", Father:";); + } + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) { + STRACE("causality", tout << " #" << substituted->get_owner_id();); + } + else { + STRACE("causality", tout << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";); + } + } + if (used_enodes.size() > 0) { + STRACE("causality", tout << "\n";); + } + } + } + void log_add_instance( fingerprint* f, quantifier * q, app * pat, @@ -261,6 +294,7 @@ namespace smt { unsigned min_top_generation, unsigned max_top_generation, vector> & used_enodes) { + max_generation = std::max(max_generation, get_generation(q)); if (m_num_instances > m_params.m_qi_max_instances) { return false; @@ -268,6 +302,9 @@ namespace smt { get_stat(q)->update_max_generation(max_generation); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); if (f) { + if (is_trace_enabled("causality")) { + log_causality(f,pat,used_enodes); + } if (has_trace_stream()) { log_add_instance(f, q, pat, num_bindings, bindings, used_enodes); } diff --git a/src/smt/smt_quantifier_stat.cpp b/src/smt/smt_quantifier_stat.cpp index 8c7fd196e..78c0124c3 100644 --- a/src/smt/smt_quantifier_stat.cpp +++ b/src/smt/smt_quantifier_stat.cpp @@ -27,6 +27,8 @@ namespace smt { m_case_split_factor(1), m_num_nested_quantifiers(0), m_num_instances(0), + m_num_instances_checker_sat(0), + m_num_instances_simplify_true(0), m_num_instances_curr_search(0), m_num_instances_curr_branch(0), m_max_generation(0), diff --git a/src/smt/smt_quantifier_stat.h b/src/smt/smt_quantifier_stat.h index c30881579..ffa20cb43 100644 --- a/src/smt/smt_quantifier_stat.h +++ b/src/smt/smt_quantifier_stat.h @@ -36,6 +36,8 @@ namespace smt { unsigned m_case_split_factor; //!< the product of the size of the clauses created by this quantifier. unsigned m_num_nested_quantifiers; unsigned m_num_instances; + unsigned m_num_instances_checker_sat; + unsigned m_num_instances_simplify_true; unsigned m_num_instances_curr_search; unsigned m_num_instances_curr_branch; //!< only updated if QI_TRACK_INSTANCES is true unsigned m_max_generation; //!< max. generation of an instance @@ -69,6 +71,12 @@ namespace smt { unsigned get_num_instances() const { return m_num_instances; } + unsigned get_num_instances_simplify_true() const { + return m_num_instances_simplify_true; + } + unsigned get_num_instances_checker_sat() const { + return m_num_instances_checker_sat; + } unsigned get_num_instances_curr_search() const { return m_num_instances_curr_search; @@ -77,6 +85,14 @@ namespace smt { unsigned & get_num_instances_curr_branch() { return m_num_instances_curr_branch; } + + void inc_num_instances_simplify_true() { + m_num_instances_simplify_true++; + } + + void inc_num_instances_checker_sat() { + m_num_instances_checker_sat++; + } void inc_num_instances() { m_num_instances++; diff --git a/src/util/trace.h b/src/util/trace.h index 1805f5657..fad4707c0 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -52,4 +52,6 @@ static inline void finalize_trace() {} #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); }) +#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { CODE tout.flush(); }) + #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })