From 8da1b024b7fc2352839b7783d498517d8b11106e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Mar 2019 04:30:29 -0700 Subject: [PATCH] fix #2205 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 - src/ast/datatype_decl_plugin.cpp | 19 ++++++----- src/ast/rewriter/th_rewriter.cpp | 1 + src/smt/smt_theory.cpp | 51 +++++++++++++++++++++++++++++ src/smt/smt_theory.h | 56 +++++--------------------------- src/smt/theory_datatype.cpp | 2 +- 6 files changed, 71 insertions(+), 59 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c73e2f1d8..68d24d0a9 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1875,7 +1875,6 @@ void ast_manager::delete_node(ast * n) { while ((n = m_ast_table.pop_erase())) { - TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 146c7359f..71b35f914 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -454,23 +454,24 @@ namespace datatype { } void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) { + std::ostream& out = m_manager->trace_stream(); symbol const& family_name = m_manager->get_family_name(get_family_id()); for (constructor const* c : *m_defs[s]) { func_decl_ref f = c->instantiate(new_sort); const unsigned num_args = f->get_arity(); if (num_args == 0) continue; for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; + out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; ++m_id_counter; } const unsigned constructor_id = m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); + out << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; + out << " " << family_name << "#" << constructor_id - num_args + i; } - m_manager->trace_stream() << "\n"; + out << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; + out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; ++m_id_counter; m_axiom_bases.insert(f->get_name(), constructor_id + 4); std::ostringstream var_sorts; @@ -481,14 +482,14 @@ namespace datatype { unsigned i = 0; for (accessor const* a : *c) { func_decl_ref acc = a->instantiate(new_sort); - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; + out << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i + out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i << " " << family_name << "#" << m_id_counter - 1 << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 + out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n"; - m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; + out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; ++m_id_counter; ++i; } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 1b586b4b6..9390e21ee 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; m().trace_stream() << "[end-of-instance]\n"; + m().trace_stream().flush(); } if (st != BR_DONE && st != BR_FAILED) { diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 63c6d7417..b791991f2 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -137,5 +137,56 @@ namespace smt { theory::~theory() { } + + void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector> & used_enodes) { + ast_manager & m = get_manager(); + std::ostream& out = m.trace_stream(); + symbol const & family_name = m.get_family_name(get_family_id()); + if (pattern_id == UINT_MAX) { + out << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << family_name << "#"; + if (axiom_id != UINT_MAX) + out << axiom_id; + for (unsigned i = 0; i < num_bindings; ++i) { + out << " #" << bindings[i]->get_id(); + } + if (used_enodes.size() > 0) { + out << " ;"; + for (auto n : used_enodes) { + enode *substituted = std::get<1>(n); + SASSERT(std::get<0>(n) == nullptr); + out << " #" << substituted->get_owner_id(); + } + } + } else { + SASSERT(axiom_id != UINT_MAX); + obj_hashtable already_visited; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + quantifier_manager::log_justification_to_root(out, orig, already_visited, get_context(), get_manager()); + quantifier_manager::log_justification_to_root(out, substituted, already_visited, get_context(), get_manager()); + } + } + out << "[new-match] " << static_cast(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id; + for (unsigned i = 0; i < num_bindings; ++i) { + out << " #" << bindings[i]->get_id(); + } + out << " ;"; + 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"; + out << "[instance] " << static_cast(nullptr) << " #" << r->get_id() << "\n"; + out.flush(); + } + }; diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index f1f304fa6..92aa87163 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -360,55 +360,15 @@ namespace smt { std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); } protected: - void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { - ast_manager & m = get_manager(); - symbol const & family_name = m.get_family_name(get_family_id()); - if (pattern_id == UINT_MAX) { - m.trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << family_name << "#"; - if (axiom_id != UINT_MAX) - m.trace_stream() << axiom_id; - for (unsigned i = 0; i < num_bindings; ++i) { - m.trace_stream() << " #" << bindings[i]->get_id(); - } - if (used_enodes.size() > 0) { - m.trace_stream() << " ;"; - for (auto n : used_enodes) { - enode *substituted = std::get<1>(n); - SASSERT(std::get<0>(n) == nullptr); - m.trace_stream() << " #" << substituted->get_owner_id(); - } - } - } else { - SASSERT(axiom_id != UINT_MAX); - obj_hashtable already_visited; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig != nullptr) { - quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager()); - quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager()); - } - } - m.trace_stream() << "[new-match] " << static_cast(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id; - for (unsigned i = 0; i < num_bindings; ++i) { - m.trace_stream() << " #" << bindings[i]->get_id(); - } - m.trace_stream() << " ;"; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig == nullptr) { - m.trace_stream() << " #" << substituted->get_owner_id(); - } else { - m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; - } - } - } - m.trace_stream() << "\n"; - m.trace_stream() << "[instance] " << static_cast(nullptr) << " #" << r->get_id() << "\n"; - } + void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, + app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + const vector> & used_enodes = vector>()); - void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); } + void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, + app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + const vector> & used_enodes = vector>()) { + log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); + } void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) { vector> used_enodes; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index f26791639..9e941fcd5 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -139,7 +139,7 @@ namespace smt { expr * acc = m.mk_app(d, n->get_owner()); args.push_back(acc); } - expr * mk = m.mk_app(c, args.size(), args.c_ptr()); + expr_ref mk(m.mk_app(c, args.size(), args.c_ptr()), m); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_eq(n->get_owner(), mk);