mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
print skolem declarations only for lemma tracing
This commit is contained in:
parent
791ca02ab1
commit
786280c646
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue