From 7ead159b2d90df2a3ff089d9d80108d4a19e7666 Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Tue, 9 Apr 2019 16:54:54 +0200 Subject: [PATCH 1/3] comments for log_axiom_definitions --- src/ast/datatype_decl_plugin.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8bf0abbb3..8c755335e 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -459,6 +459,8 @@ namespace datatype { func_decl_ref f = c->instantiate(new_sort); const unsigned num_args = f->get_arity(); if (num_args == 0) continue; + + // log constructor with quantified variables as arguments for (unsigned i = 0; i < num_args; ++i) { m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; ++m_id_counter; @@ -470,6 +472,8 @@ namespace datatype { } m_manager->trace_stream() << "\n"; ++m_id_counter; + + // axioms for all accessors are generated when a constructor is applied => use constructor as pattern m_manager->trace_stream() << "[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); @@ -478,6 +482,8 @@ namespace datatype { var_sorts << " (;" << a->range()->get_name() << ")"; } std::string var_description = var_sorts.str(); + + // create axioms: the ith accessor returns the ith argument of the constructor unsigned i = 0; for (accessor const* a : *c) { func_decl_ref acc = a->instantiate(new_sort); From 1c24d340d136aa3956e33277018cc2a8f590912c Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Thu, 18 Apr 2019 14:45:43 +0200 Subject: [PATCH 2/3] fixing bug causing unbalance between [instance] and [end-of-instance] lines --- src/smt/qi_queue.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index d621a9f50..88d1f73e7 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -216,8 +216,10 @@ namespace smt { if (m_manager.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream()) { + display_instance_profile(f, q, num_bindings, bindings, pr->get_id(), generation); m_manager.trace_stream() << "[end-of-instance]\n"; + } return; } From bd974799fccbe702137c70c50423f1482946aab6 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 20 Apr 2019 17:41:03 +0200 Subject: [PATCH 3/3] adding #qvars to [mk-quant] log line --- src/ast/ast.cpp | 2 +- src/ast/datatype_decl_plugin.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 68d24d0a9..e358c5fe1 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2443,7 +2443,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector &args) { static void trace_quant(std::ostream& strm, quantifier* q) { strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]") - << " #" << q->get_id() << " " << q->get_qid(); + << " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls(); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { strm << " #" << q->get_pattern(i)->get_id(); } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index e3a1c9ed6..4bc9b5170 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -494,8 +494,8 @@ namespace datatype { 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; - out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 - << " " << family_name << "#" << m_id_counter - 1 << "\n"; + out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << num_args << " " << family_name + << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n"; out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; ++m_id_counter; ++i;