From 1894c86ee015eafbacb0730d44d625034271d6e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Aug 2022 18:27:30 -0700 Subject: [PATCH] virtual Signed-off-by: Nikolaj Bjorner --- src/sat/sat_drat.cpp | 14 ++++++++------ src/sat/sat_drat.h | 10 +++++++--- src/sat/smt/euf_proof.cpp | 35 ++++++++++++++++++++++++----------- src/sat/smt/euf_solver.cpp | 9 ++------- src/sat/smt/euf_solver.h | 7 +++++-- 5 files changed, 46 insertions(+), 29 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 3b52b0f7f..0633612ad 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -35,7 +35,6 @@ namespace sat { if (s.get_config().m_drat_binary) std::swap(m_out, m_bout); } - // m_print_clause = nullptr; } drat::~drat() { @@ -684,6 +683,7 @@ namespace sat { verify(0, nullptr); SASSERT(m_inconsistent); } + if (m_print_clause) m_print_clause->on_clause(0, nullptr, status::redundant()); } void drat::add(literal l, bool learned) { ++m_stats.m_num_add; @@ -691,7 +691,7 @@ namespace sat { if (m_out) dump(1, &l, st); if (m_bout) bdump(1, &l, st); if (m_check) append(l, st); - //if (m_print_clause) m_print_clause(1, &l, st); + if (m_print_clause) m_print_clause->on_clause(1, &l, st); } void drat::add(literal l1, literal l2, status st) { if (st.is_deleted()) @@ -702,7 +702,7 @@ namespace sat { if (m_out) dump(2, ls, st); if (m_bout) bdump(2, ls, st); if (m_check) append(l1, l2, st); - //if (m_print_clause) m_print_clause(2, ls, st); + if (m_print_clause) m_print_clause->on_clause(2, ls, st); } void drat::add(clause& c, status st) { if (st.is_deleted()) @@ -712,7 +712,7 @@ namespace sat { if (m_out) dump(c.size(), c.begin(), st); if (m_bout) bdump(c.size(), c.begin(), st); if (m_check) append(mk_clause(c), st); - //if (m_print_clause) m_print_clause(c.size(), c.begin(), st); + if (m_print_clause) m_print_clause->on_clause(c.size(), c.begin(), st); } void drat::add(literal_vector const& lits, status st) { @@ -734,7 +734,8 @@ namespace sat { if (m_out) dump(sz, lits, st); - //if (m_print_clause) m_print_clause(sz, lits, st); + if (m_print_clause) + m_print_clause->on_clause(sz, lits, st); } void drat::add(literal_vector const& c) { @@ -754,7 +755,8 @@ namespace sat { } } } - // if (m_print_clause) m_print_clause(c.size(), c.data(), status::redundant()); + if (m_print_clause) + m_print_clause->on_clause(c.size(), c.data(), status::redundant()); } void drat::del(literal l) { diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 046f0bbc9..e60e80487 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -60,6 +60,10 @@ namespace sat { class justification; class clause; + struct print_clause { + virtual void on_clause(unsigned, literal const*, status) = 0; + }; + class drat { struct stats { unsigned m_num_drup = 0; @@ -73,7 +77,7 @@ namespace sat { watched_clause(clause* c, literal l1, literal l2): m_clause(c), m_l1(l1), m_l2(l2) {} }; - std::function m_print_clause; + print_clause* m_print_clause = nullptr; svector m_watched_clauses; typedef svector watch; solver& s; @@ -140,8 +144,8 @@ namespace sat { void add(literal_vector const& c); // add learned clause void add(unsigned sz, literal const* lits, status st); - void set_print_clause(std::function& print_clause) { - // m_print_clause = print_clause; + void set_print_clause(print_clause& print_clause) { + m_print_clause = &print_clause; } // support for SMT - connect Boolean variables with AST nodes diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 36ed50a0b..a63efb79b 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -29,6 +29,18 @@ namespace euf { m_drat_initialized = true; } + void solver::def_add_arg(unsigned arg) { + get_drat().def_add_arg(arg); + } + + void solver::def_end() { + get_drat().def_end(); + } + + void solver::def_begin(char id, unsigned n, std::string const& name) { + get_drat().def_begin(id, n, name); + } + void solver::drat_log_params(func_decl* f) { for (unsigned i = f->get_num_parameters(); i-- > 0; ) { auto const& p = f->get_parameter(i); @@ -39,6 +51,7 @@ namespace euf { drat_log_decl(to_func_decl(a)); } } + void solver::drat_log_expr1(expr* e) { if (is_app(e)) { app* a = to_app(e); @@ -48,14 +61,14 @@ namespace euf { strm << mk_ismt2_func(a->get_decl(), m); get_drat().def_begin('e', e->get_id(), strm.str()); for (expr* arg : *a) - get_drat().def_add_arg(arg->get_id()); - get_drat().def_end(); + def_add_arg(arg->get_id()); + def_end(); } else if (is_var(e)) { var* v = to_var(e); get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m)); - get_drat().def_add_arg(v->get_idx()); - get_drat().def_end(); + def_add_arg(v->get_idx()); + def_end(); } else if (is_quantifier(e)) { quantifier* q = to_quantifier(e); @@ -65,8 +78,8 @@ namespace euf { strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")"; strm << ")"; get_drat().def_begin('q', q->get_id(), strm.str()); - get_drat().def_add_arg(q->get_expr()->get_id()); - get_drat().def_end(); + def_add_arg(q->get_expr()->get_id()); + def_end(); } else UNREACHABLE(); @@ -118,7 +131,7 @@ namespace euf { smt2_pp_environment_dbg env(m); ast_smt2_pp(strm, f, env); get_drat().def_begin('f', f->get_small_id(), strm.str()); - get_drat().def_end(); + def_end(); } /** @@ -188,13 +201,13 @@ namespace euf { drat_log_expr(a); drat_log_expr(b); get_drat().def_begin('e', eq->get_id(), std::string("=")); - get_drat().def_add_arg(a->get_id()); - get_drat().def_add_arg(b->get_id()); - get_drat().def_end(); + def_add_arg(a->get_id()); + def_add_arg(b->get_id()); + def_end(); get_drat().bool_def(lit.var(), eq->get_id()); } - void solver::log_clause(unsigned n, literal const* lits, sat::status st) { + void solver::on_clause(unsigned n, literal const* lits, sat::status st) { if (!get_config().m_lemmas2console) return; if (!st.is_redundant() && !st.is_asserted()) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 56480aa85..656249944 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -171,13 +171,8 @@ namespace euf { for (auto* s : m_solvers) s->init_search(); - if (get_config().m_lemmas2console) { - std::function on_clause = - [&](unsigned n, sat::literal const* lits, sat::status st) { - log_clause(n, lits, st); - }; - get_drat().set_print_clause(on_clause); - } + if (get_config().m_lemmas2console) + get_drat().set_print_clause(*this); } bool solver::is_external(bool_var v) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index e2cdd7862..f77954ded 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -60,7 +60,7 @@ namespace euf { std::ostream& display(std::ostream& out) const; }; - class solver : public sat::extension, public th_internalizer, public th_decompile { + class solver : public sat::extension, public th_internalizer, public th_decompile, public sat::print_clause { typedef top_sort deps_t; friend class ackerman; class user_sort; @@ -183,7 +183,10 @@ namespace euf { 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); + void on_clause(unsigned n, literal const* lits, sat::status st) override; + void def_add_arg(unsigned arg); + void def_end(); + void def_begin(char id, unsigned n, std::string const& name); // relevancy