From 23d01f5974cf6d97455f00d562fbf46da7ce218e Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Wed, 10 Jul 2019 16:17:30 +0200 Subject: [PATCH 1/5] fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with) --- src/ast/rewriter/th_rewriter.cpp | 35 ++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 0e73a362332..68fa45f725e 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -34,6 +34,8 @@ Module Name: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/well_sorted.h" +#include "ast/ast.h" +#include namespace { struct th_rewriter_cfg : public default_rewriter_cfg { @@ -557,6 +559,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return BR_DONE; } + void count_subterm_references(expr * e, map, ptr_eq> & reference_map) { + if (is_app(e)) { + app * a = to_app(e); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr * child = a->get_arg(i); + reference_map.insert(child, reference_map.get(child, 0) + 1); + } + } + } + + void log_enodes_for_new_terms(expr *term) { + map, ptr_eq> reference_map; + count_subterm_references(term, reference_map); + + // Any term that was newly introduced by the rewrite step is only referenced within the result term. + for (auto kv : reference_map) { + if (kv.m_key->get_ref_count() == kv.m_value) { + m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; + } + } + } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = nullptr; br_status st = reduce_app_core(f, num, args, result); @@ -581,8 +605,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg { result_pr = m().mk_rewrite(tmp, result); tmp = m().mk_eq(tmp, result); m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; - m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n"; - m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; + + // Make sure that both the result term and equality were newly introduced. + if (tmp->get_ref_count() == 1) { + if (result->get_ref_count() == 1) { + log_enodes_for_new_terms(result); + m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n"; + } + m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; + } m().trace_stream() << "[end-of-instance]\n"; m().trace_stream().flush(); } From b226f3a77cf63ed92539165b54b48889f8ad2289 Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Wed, 10 Jul 2019 16:43:48 +0200 Subject: [PATCH 2/5] cleaning up includes --- src/ast/rewriter/th_rewriter.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 68fa45f725e..c6439e12aee 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -34,8 +34,6 @@ Module Name: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/well_sorted.h" -#include "ast/ast.h" -#include namespace { struct th_rewriter_cfg : public default_rewriter_cfg { From 7a48524213f5935efa6579cbfacb9af60de775dd Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Wed, 10 Jul 2019 17:09:21 +0200 Subject: [PATCH 3/5] count subterm references correctly --- src/ast/rewriter/th_rewriter.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index c6439e12aee..06f64c6ff38 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -557,23 +557,26 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return BR_DONE; } - void count_subterm_references(expr * e, map, ptr_eq> & reference_map) { + void count_down_subterm_references(expr * e, map, ptr_eq> & reference_map) { if (is_app(e)) { app * a = to_app(e); for (unsigned i = 0; i < a->get_num_args(); ++i) { expr * child = a->get_arg(i); - reference_map.insert(child, reference_map.get(child, 0) + 1); + unsigned countdown = reference_map.get(child, child->get_ref_count()) - 1; + reference_map.insert(child, countdown); + if (countdown == 0) + count_down_subterm_references(child, reference_map); } } } void log_enodes_for_new_terms(expr *term) { map, ptr_eq> reference_map; - count_subterm_references(term, reference_map); + count_down_subterm_references(term, reference_map); // Any term that was newly introduced by the rewrite step is only referenced within the result term. for (auto kv : reference_map) { - if (kv.m_key->get_ref_count() == kv.m_value) { + if (kv.m_value == 0) { m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; } } From 1d859a98e571245ddfc0cbb682fb6e18ebd53993 Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Wed, 10 Jul 2019 17:12:08 +0200 Subject: [PATCH 4/5] updating comment --- src/ast/rewriter/th_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 06f64c6ff38..d09de7e5f2c 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -574,7 +574,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { map, ptr_eq> reference_map; count_down_subterm_references(term, reference_map); - // Any term that was newly introduced by the rewrite step is only referenced within the result term. + // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term. for (auto kv : reference_map) { if (kv.m_value == 0) { m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; From 335072eda2fd56974dc3fc969329f748523bec1f Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Thu, 11 Jul 2019 17:22:03 +0200 Subject: [PATCH 5/5] extract logging into separate function --- src/ast/rewriter/th_rewriter.cpp | 77 ++++++++++++++++---------------- 1 file changed, 39 insertions(+), 38 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index d09de7e5f2c..dcb995adae8 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -570,16 +570,46 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } } - void log_enodes_for_new_terms(expr *term) { - map, ptr_eq> reference_map; - count_down_subterm_references(term, reference_map); - - // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term. - for (auto kv : reference_map) { - if (kv.m_value == 0) { - m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; + void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + family_id fid = f->get_family_id(); + if (fid == m_b_rw.get_fid()) { + decl_kind k = f->get_decl_kind(); + if (k == OP_EQ) { + SASSERT(num == 2); + fid = m().get_sort(args[0])->get_family_id(); + } + else if (k == OP_ITE) { + SASSERT(num == 3); + fid = m().get_sort(args[1])->get_family_id(); + } + } + app_ref tmp(m()); + tmp = m().mk_app(f, num, args); + m().trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n"; + if (m().proofs_enabled()) + result_pr = m().mk_rewrite(tmp, result); + tmp = m().mk_eq(tmp, result); + m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; + + // Make sure that both the result term and equality were newly introduced. + if (tmp->get_ref_count() == 1) { + if (result->get_ref_count() == 1) { + map, ptr_eq> reference_map; + count_down_subterm_references(result, reference_map); + + // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term. + for (auto kv : reference_map) { + if (kv.m_value == 0) { + m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; + } + } + + m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n"; } + m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; } + m().trace_stream() << "[end-of-instance]\n"; + m().trace_stream().flush(); } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -587,36 +617,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { br_status st = reduce_app_core(f, num, args, result); if (st != BR_FAILED && m().has_trace_stream()) { - family_id fid = f->get_family_id(); - if (fid == m_b_rw.get_fid()) { - decl_kind k = f->get_decl_kind(); - if (k == OP_EQ) { - SASSERT(num == 2); - fid = m().get_sort(args[0])->get_family_id(); - } - else if (k == OP_ITE) { - SASSERT(num == 3); - fid = m().get_sort(args[1])->get_family_id(); - } - } - app_ref tmp(m()); - tmp = m().mk_app(f, num, args); - m().trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n"; - if (m().proofs_enabled()) - result_pr = m().mk_rewrite(tmp, result); - tmp = m().mk_eq(tmp, result); - m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; - - // Make sure that both the result term and equality were newly introduced. - if (tmp->get_ref_count() == 1) { - if (result->get_ref_count() == 1) { - log_enodes_for_new_terms(result); - m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n"; - } - m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; - } - m().trace_stream() << "[end-of-instance]\n"; - m().trace_stream().flush(); + log_rewrite_axiom_instantiation(f, num, args, result, result_pr); } if (st != BR_DONE && st != BR_FAILED) {