From 7b3a634b8de2c3134c11df26baebb6e0b17a7477 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Oct 2022 07:54:49 -0700 Subject: [PATCH] wip - features and bug-fixes to proof logging --- src/ast/euf/euf_egraph.cpp | 2 +- src/sat/sat_solver.cpp | 14 +++++++++----- src/sat/smt/distinct_theory_checker.h | 2 +- src/sat/smt/euf_internalize.cpp | 2 +- src/sat/smt/euf_proof.cpp | 17 ++++++++--------- src/sat/smt/euf_proof_checker.cpp | 18 ++++++++---------- src/sat/smt/euf_proof_checker.h | 5 +++-- src/sat/smt/euf_solver.cpp | 15 +++++---------- src/sat/smt/euf_solver.h | 9 ++++++--- src/sat/smt/sat_th.cpp | 2 ++ src/sat/smt/sat_th.h | 2 +- 11 files changed, 45 insertions(+), 43 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 8f04b1b00..6034d8428 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -650,7 +650,7 @@ namespace euf { SASSERT(n1->get_decl() == n2->get_decl()); m_uses_congruence = true; if (m_used_cc && !comm) { - m_used_cc(to_app(n1->get_expr()), to_app(n2->get_expr())); + m_used_cc(n1->get_app(), n2->get_app()); } if (comm && n1->get_arg(0)->get_root() == n2->get_arg(1)->get_root() && diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8f9938dbb..15bc20a58 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -432,15 +432,17 @@ namespace sat { m_mc.add_clause(num_lits, lits); } - switch (num_lits) { case 0: set_conflict(); return nullptr; case 1: - if (!logged && m_config.m_drat && (!st.is_sat() || st.is_input())) + if (!logged && m_config.m_drat) drat_log_clause(num_lits, lits, st); - assign_unit(lits[0]); + { + flet _disable_drat(m_config.m_drat, false); + assign(lits[0], justification(0)); + } return nullptr; case 2: mk_bin_clause(lits[0], lits[1], st); @@ -460,6 +462,9 @@ namespace sat { bool redundant = st.is_redundant(); m_touched[l1.var()] = m_touch_index; m_touched[l2.var()] = m_touch_index; + + if (m_config.m_drat) + m_drat.add(l1, l2, st); if (redundant && !m_trim && find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) { assign_unit(l1); @@ -484,8 +489,7 @@ namespace sat { push_reinit_stack(l1, l2); return; } - if (m_config.m_drat) - m_drat.add(l1, l2, st); + if (propagate_bin_clause(l1, l2)) { if (!at_base_lvl()) push_reinit_stack(l1, l2); diff --git a/src/sat/smt/distinct_theory_checker.h b/src/sat/smt/distinct_theory_checker.h index a2fb366f7..81092b445 100644 --- a/src/sat/smt/distinct_theory_checker.h +++ b/src/sat/smt/distinct_theory_checker.h @@ -42,7 +42,7 @@ namespace distinct { bool check(app* jst) override { return true; } void register_plugins(euf::theory_checker& pc) override { - pc.register_plugin(symbol("distinct"), this); + pc.register_plugin(symbol("alldiff"), this); } }; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 1bad6fc6b..a03af92c7 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -288,7 +288,7 @@ namespace euf { func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m); for (unsigned i = 0; i < sz; ++i) { expr_ref fapp(m.mk_app(f, e->get_arg(i)), m); - expr_ref fresh(m.mk_fresh_const("dist-value", u), m); + expr_ref fresh(m.mk_model_value(i, u), m); enode* n = mk_enode(fresh, 0, nullptr); n->mark_interpreted(); expr_ref eq = mk_eq(fapp, fresh); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 4f2677208..3e42d130e 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -73,20 +73,20 @@ namespace euf { } } - eq_proof_hint* solver::mk_hint(literal lit, literal_vector const& r) { + eq_proof_hint* solver::mk_hint(symbol const& th, literal conseq, literal_vector const& r) { if (!use_drat()) return nullptr; push(value_trail(m_lit_tail)); push(value_trail(m_cc_tail)); push(restore_size_trail(m_proof_literals)); - if (lit != sat::null_literal) - m_proof_literals.push_back(~lit); + if (conseq != sat::null_literal) + m_proof_literals.push_back(~conseq); m_proof_literals.append(r); m_lit_head = m_lit_tail; m_cc_head = m_cc_tail; m_lit_tail = m_proof_literals.size(); m_cc_tail = m_explain_cc.size(); - return new (get_region()) eq_proof_hint(m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); + return new (get_region()) eq_proof_hint(th, m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); } th_proof_hint* solver::mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b) { @@ -107,7 +107,7 @@ namespace euf { m_cc_head = m_cc_tail; m_lit_tail = m_proof_literals.size(); m_cc_tail = m_explain_cc.size(); - return new (get_region()) eq_proof_hint(m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); + return new (get_region()) eq_proof_hint(m_euf, m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); } th_proof_hint* solver::mk_tc_proof_hint(sat::literal const* clause) { @@ -119,13 +119,12 @@ namespace euf { for (unsigned i = 0; i < 3; ++i) m_proof_literals.push_back(~clause[i]); - m_lit_head = m_lit_tail; m_cc_head = m_cc_tail; m_lit_tail = m_proof_literals.size(); m_cc_tail = m_explain_cc.size(); - return new (get_region()) eq_proof_hint(m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); + return new (get_region()) eq_proof_hint(m_euf, m_lit_head, m_lit_tail, m_cc_head, m_cc_tail); } @@ -162,7 +161,7 @@ namespace euf { for (auto * arg : args) sorts.push_back(arg->get_sort()); - func_decl* f = m.mk_func_decl(symbol("euf"), sorts.size(), sorts.data(), proof); + func_decl* f = m.mk_func_decl(th, sorts.size(), sorts.data(), proof); return m.mk_app(f, args); } @@ -239,7 +238,7 @@ namespace euf { } sat::status solver::mk_distinct_status(unsigned n, sat::literal const* lits) { - th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("distinct"), n, lits) : nullptr; + th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("alldiff"), n, lits) : nullptr; return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); } diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index c6218f2fe..ff2803cb8 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -396,17 +396,15 @@ namespace euf { void smt_proof_checker::log_verified(app* proof_hint) { symbol n = proof_hint->get_name(); - if (n == m_last_rule) { - ++m_num_last_rules; - return; - } - if (m_num_last_rules > 0) - std::cout << "(verified-" << m_last_rule << "+" << m_num_last_rules << ")\n"; - - std::cout << "(verified-" << n << ")\n"; - m_last_rule = n; - m_num_last_rules = 0; + m_hint2hit.insert_if_not_there(n, 0)++; + ++m_num_logs; + if (m_num_logs < 100 || (m_num_logs % 1000) == 0) { + std::cout << "(verified"; + for (auto const& [k, v] : m_hint2hit) + std::cout << " :" << k << " " << v; + std::cout << ")\n"; + } } bool smt_proof_checker::check_rup(expr_ref_vector const& clause) { diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index 6d5cb3290..ae8b9a407 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -90,8 +90,9 @@ namespace euf { bool m_check_rup = false; // for logging - symbol m_last_rule; - unsigned m_num_last_rules = 0; + + map m_hint2hit; + unsigned m_num_logs = 0; void add_units() { auto const& units = m_drat.units(); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index f0d40a13f..b462998a2 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -225,8 +225,9 @@ namespace euf { void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) { m_egraph.begin_explain(); m_explain.reset(); - if (use_drat() && !probing) + if (use_drat() && !probing) { push(restore_size_trail(m_explain_cc, m_explain_cc.size())); + } auto* ext = sat::constraint_base::to_extension(idx); th_proof_hint* hint = nullptr; bool has_theory = false; @@ -252,15 +253,9 @@ namespace euf { } } m_egraph.end_explain(); - if (use_drat() && !probing) { - if (!has_theory) - hint = mk_hint(l, r); - else { - if (l != sat::null_literal) r.push_back(~l); - hint = mk_smt_hint(symbol("smt"), r); - if (l != sat::null_literal) r.pop_back(); - } - } + if (use_drat() && !probing) + hint = mk_hint(has_theory ? m_smt : m_euf, l, r); + unsigned j = 0; for (sat::literal lit : r) if (s().lvl(lit) > 0) r[j++] = lit; diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index f4109bed1..b423b1768 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -62,10 +62,11 @@ namespace euf { }; class eq_proof_hint : public th_proof_hint { + symbol th; unsigned m_lit_head, m_lit_tail, m_cc_head, m_cc_tail; public: - eq_proof_hint(unsigned lh, unsigned lt, unsigned ch, unsigned ct): - m_lit_head(lh), m_lit_tail(lt), m_cc_head(ch), m_cc_tail(ct) {} + eq_proof_hint(symbol const& th, unsigned lh, unsigned lt, unsigned ch, unsigned ct): + th(th), m_lit_head(lh), m_lit_tail(lt), m_cc_head(ch), m_cc_tail(ct) {} expr* get_hint(euf::solver& s) const override; }; @@ -202,7 +203,9 @@ namespace euf { svector m_proof_eqs, m_proof_deqs, m_expr_pairs; unsigned m_lit_head = 0, m_lit_tail = 0, m_cc_head = 0, m_cc_tail = 0; unsigned m_eq_head = 0, m_eq_tail = 0, m_deq_head = 0, m_deq_tail = 0; - eq_proof_hint* mk_hint(literal lit, literal_vector const& r); + symbol m_euf = symbol("euf"); + symbol m_smt = symbol("smt"); + eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r); bool m_proof_initialized = false; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index ad280eff8..81fd7e384 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -130,6 +130,8 @@ namespace euf { } bool th_euf_solver::add_unit(sat::literal lit, th_proof_hint const* ps) { + if (ctx.use_drat() && !ps) + ps = ctx.mk_smt_clause(name(), 1, &lit); bool was_true = is_true(lit); ctx.s().add_clause(1, &lit, mk_status(ps)); ctx.add_root(lit); diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 532d04a2e..d64b65635 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -238,7 +238,7 @@ namespace euf { public: static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr); - static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, th_proof_hint const* ph = nullptr) { return conflict(th, lits.size(), lits.data(), 0, nullptr, nullptr); } + static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, th_proof_hint const* ph = nullptr) { return conflict(th, lits.size(), lits.data(), 0, nullptr, ph); } static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, th_proof_hint const* ph = nullptr); static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr); static th_explain* conflict(th_euf_solver& th, sat::literal lit, th_proof_hint const* ph = nullptr);