print skolem declarations only for lemma tracing

Z3Prover · Aug 11, 2022 · 786280c · 786280c
1 parent 791ca02
commit 786280c
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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);
         }
 
     }