From 786280c646af41a1397bd7119f1dd42276b50868 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Aug 2022 11:34:54 +0300 Subject: [PATCH] print skolem declarations only for lemma tracing --- src/ast/ast_pp_util.cpp | 11 +++++++++++ src/ast/ast_pp_util.h | 2 ++ src/smt/smt_internalizer.cpp | 4 ++-- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 008a7cc9a..c895b8fe8 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -64,6 +64,17 @@ void ast_pp_util::display_decls(std::ostream& out) { m_rec_decls = n; } +void ast_pp_util::display_skolem_decls(std::ostream& out) { + ast_smt_pp pp(m); + unsigned n = coll.get_num_decls(); + for (unsigned i = m_decls; i < n; ++i) { + func_decl* f = coll.get_func_decls()[i]; + if (f->get_family_id() == null_family_id && !m_removed.contains(f) && f->is_skolem()) + ast_smt2_pp(out, f, m_env) << "\n"; + } + m_decls = n; +} + void ast_pp_util::remove_decl(func_decl* f) { m_removed.insert(f); } diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index 06ade7eed..6b5c5103e 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -50,6 +50,8 @@ class ast_pp_util { void display_decls(std::ostream& out); + void display_skolem_decls(std::ostream& out); + void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true); void display_assert(std::ostream& out, expr* f, bool neat = true); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 648ea9b7e..d86594f0f 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1529,8 +1529,8 @@ namespace smt { fmls.push_back(literal2expr(lits[i])); fml = mk_or(fmls); m_lemma_visitor.collect(fml); - m_lemma_visitor.display_decls(std::cout); - m_lemma_visitor.display_assert(std::cout, fml.get(), false); + m_lemma_visitor.display_skolem_decls(std::cout); + m_lemma_visitor.display_assert(std::cout, fml.get(), true); } }