From fb8532bf55a63e9cb53cbe7d3d4aa825ed73bccb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Aug 2022 21:06:04 -0700 Subject: [PATCH] succinct logging Signed-off-by: Nikolaj Bjorner --- src/ast/ast_pp_util.cpp | 47 ++++++++++++++++++++++++++++++++++++++ src/ast/ast_pp_util.h | 9 ++++++-- src/sat/smt/euf_proof.cpp | 39 +++++++++++++++++++------------ src/sat/smt/euf_solver.cpp | 3 ++- src/sat/smt/euf_solver.h | 1 + 5 files changed, 81 insertions(+), 18 deletions(-) diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index c895b8fe8..a6f81131e 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -129,6 +129,7 @@ void ast_pp_util::push() { m_rec_decls.push(); m_decls.push(); m_sorts.push(); + m_defined_lim.push_back(m_defined.size()); } void ast_pp_util::pop(unsigned n) { @@ -136,4 +137,50 @@ void ast_pp_util::pop(unsigned n) { m_rec_decls.pop(n); m_decls.pop(n); m_sorts.pop(n); + unsigned old_sz = m_defined_lim[m_defined_lim.size() - n]; + for (unsigned i = m_defined.size(); i-- > old_sz; ) + m_is_defined.mark(m_defined[i], false); + m_defined.shrink(old_sz); + m_defined_lim.shrink(m_defined_lim.size() - n); +} + +std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) { + ptr_buffer visit; + visit.push_back(n); + while (!visit.empty()) { + n = visit.back(); + if (m_is_defined.is_marked(n)) { + visit.pop_back(); + continue; + } + if (is_app(n)) { + bool all_visit = true; + for (auto* e : *to_app(n)) { + if (m_is_defined.is_marked(e)) + continue; + all_visit = false; + visit.push_back(e); + } + if (!all_visit) + continue; + m_defined.push_back(n); + m_is_defined.mark(n, true); + visit.pop_back(); + if (to_app(n)->get_num_args() == 0) + out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n"; + else { + out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " ("; + out << to_app(n)->get_name(); // fixme + for (auto* e : *to_app(n)) + out << " $" << e->get_id(); + out << ")\n"; + } + continue; + } + out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n"; + m_defined.push_back(n); + m_is_defined.mark(n, true); + visit.pop_back(); + } + return out; } diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index 6b5c5103e..7dcc21a7b 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -30,6 +30,9 @@ class ast_pp_util { stacked_value m_rec_decls; stacked_value m_decls; stacked_value m_sorts; + expr_mark m_is_defined; + ptr_vector m_defined; + unsigned_vector m_defined_lim; public: @@ -37,8 +40,8 @@ class ast_pp_util { ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m) {} - void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); } - + void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); + m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); } void collect(expr* e); @@ -60,6 +63,8 @@ class ast_pp_util { std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true); + std::ostream& define_expr(std::ostream& out, expr* f); + void push(); void pop(unsigned n); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index dd4340c2b..da11929da 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -195,22 +195,31 @@ namespace euf { } void solver::log_clause(unsigned n, literal const* lits, sat::status st) { - if (get_config().m_lemmas2console) { - std::function ppth = [&](int th) { - return m.get_family_name(th); - }; - if (st.is_redundant() || st.is_asserted()) { - expr_ref_vector clause(m); - for (unsigned i = 0; i < n; ++i) { - expr_ref e = literal2expr(lits[i]); - if (!e) - return; - clause.push_back(e); - } - expr_ref cl = mk_or(clause); - std::cout << sat::status_pp(st, ppth) << " " << cl << "\n"; - } + if (!get_config().m_lemmas2console) + return; + if (!st.is_redundant() && !st.is_asserted()) + return; + std::function ppth = [&](int th) { + return m.get_family_name(th); + }; + + expr_ref_vector clause(m); + for (unsigned i = 0; i < n; ++i) { + expr_ref e = literal2expr(lits[i]); + if (!e) + return; + clause.push_back(e); + m_clause_visitor.collect(e); } + m_clause_visitor.display_skolem_decls(std::cout); + for (expr* e : clause) + m_clause_visitor.define_expr(std::cout, e); + if (!st.is_sat()) + std::cout << "; " << sat::status_pp(st, ppth) << "\n"; + std::cout << "(assert (or"; + for (expr* e : clause) + std::cout << " $" << e->get_id(); + std::cout << "))\n"; } } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 2c4357900..56480aa85 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -49,7 +49,8 @@ namespace euf { m_lookahead(nullptr), m_to_m(&m), m_to_si(&si), - m_values(m) + m_values(m), + m_clause_visitor(m) { updt_params(p); m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d968139a7..c3ec47f13 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -182,6 +182,7 @@ namespace euf { obj_hashtable m_drat_asts; bool m_drat_initialized{ false }; void init_drat(); + ast_pp_util m_clause_visitor; void log_clause(unsigned n, literal const* lits, sat::status st); // relevancy