From bfb554c0b8e87b094ecde74196061ef1744dc150 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 14 Jan 2019 21:28:06 +0100 Subject: [PATCH] logging sorts of quantified variables logging proof objects seperately form regular terms renaming inst-possible -> inst-discovered --- src/ast/ast.cpp | 11 +++++++++-- src/smt/smt_quantifier.cpp | 2 +- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ab37a9f40..ba5ee5d5a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2202,7 +2202,14 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const } if (m_trace_stream && r == new_node) { - *m_trace_stream << "[mk-app] #" << r->get_id() << " "; + if (is_proof(r)) { + if (decl == mk_func_decl(m_basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast(nullptr))) + return r; + *m_trace_stream << "[mk-proof] #"; + } else { + *m_trace_stream << "[mk-app] #"; + } + *m_trace_stream << r->get_id() << " "; if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") { ast_ll_pp(*m_trace_stream, *this, r); } @@ -2479,7 +2486,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s trace_quant(*m_trace_stream, r); *m_trace_stream << "[attach-var-names] #" << r->get_id(); for (unsigned i = 0; i < num_decls; ++i) { - *m_trace_stream << " " << decl_names[num_decls - i - 1].str(); + *m_trace_stream << " (" << decl_names[num_decls - i - 1].str() << " ; " << decl_sorts[num_decls - i -1]->get_name().str() << ")"; } *m_trace_stream << "\n"; } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index a22889b24..65a6db875 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -212,7 +212,7 @@ namespace smt { if (f) { if (has_trace_stream()) { if (pat == nullptr) { - trace_stream() << "[inst-possible] MBQI " << static_cast(f) << " #" << q->get_id(); + trace_stream() << "[inst-discovered] MBQI " << static_cast(f) << " #" << q->get_id(); for (unsigned i = 0; i < num_bindings; ++i) { trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id(); }