From 6188c536ef852633571b34e74efe962b942f6ad7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Nov 2022 08:01:15 +0700 Subject: [PATCH] add logging of propagations to smt core log theory propagations with annotation "smt". It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core. --- src/smt/qi_queue.cpp | 2 +- src/smt/smt_clause_proof.cpp | 80 ++++++++++++++++++++++++++--- src/smt/smt_clause_proof.h | 16 ++++-- src/smt/smt_conflict_resolution.cpp | 1 + src/smt/smt_context.cpp | 5 +- src/smt/smt_context.h | 4 +- src/smt/smt_internalizer.cpp | 4 +- 7 files changed, 95 insertions(+), 17 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index cb28f87f8..582bcc664 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -304,7 +304,7 @@ namespace smt { } m_instances.push_back(pr1); } - else if (m_context.on_clause_active()) { + else if (m_context.clause_proof_active()) { expr_ref_vector bindings_e(m), args(m); arith_util a(m); expr_ref gen(a.mk_int(generation), m); diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index ad3d3818c..096a0994f 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -18,7 +18,17 @@ Revision History: #include "ast/ast_ll_pp.h" namespace smt { - clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {} + + clause_proof::clause_proof(context& ctx): + ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) { + auto proof_log = ctx.get_fparams().m_proof_log; + m_enabled = ctx.get_fparams().m_clause_proof || proof_log.is_non_empty_string(); + if (proof_log.is_non_empty_string()) { + m_pp_out = alloc(std::ofstream, proof_log.str()); + if (!*m_pp_out) + throw default_exception(std::string("Could not open file ") + proof_log.str()); + } + } clause_proof::status clause_proof::kind2st(clause_kind k) { switch (k) { @@ -42,7 +52,7 @@ namespace smt { r = j->mk_proof(ctx.get_cr()); if (r) return r; - if (!m_on_clause_active) + if (!is_enabled()) return nullptr; switch (st) { case status::assumption: @@ -60,7 +70,7 @@ namespace smt { } void clause_proof::add(clause& c) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; justification* j = c.get_justification(); auto st = kind2st(c.get_kind()); @@ -70,7 +80,7 @@ namespace smt { } void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; auto st = kind2st(k); proof_ref pr(justification2proof(st, j), m); @@ -83,7 +93,7 @@ namespace smt { void clause_proof::shrink(clause& c, unsigned new_size) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; m_lits.reset(); for (unsigned i = 0; i < new_size; ++i) @@ -97,7 +107,7 @@ namespace smt { } void clause_proof::add(literal lit, clause_kind k, justification* j) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; m_lits.reset(); m_lits.push_back(ctx.literal2expr(lit)); @@ -107,7 +117,7 @@ namespace smt { } void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; m_lits.reset(); m_lits.push_back(ctx.literal2expr(lit1)); @@ -117,21 +127,75 @@ namespace smt { update(st, m_lits, pr); } + void clause_proof::propagate(literal lit, justification const& jst, literal_vector const& ante) { + if (!is_enabled()) + return; + m_lits.reset(); + for (literal l : ante) + m_lits.push_back(ctx.literal2expr(~l)); + m_lits.push_back(ctx.literal2expr(lit)); + proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m); + update(clause_proof::status::th_lemma, m_lits, pr); + } void clause_proof::del(clause& c) { update(c, status::deleted, justification2proof(status::deleted, nullptr)); } + std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) { + for (expr* e : v) + if (m.is_not(e, e)) + m_pp.display_expr_def(out << " (not ", e) << ")"; + else + m_pp.display_expr_def(out << " ", e); + return out; + } + + std::ostream& clause_proof::display_hint(std::ostream& out, proof* p) { + if (p) + m_pp.display_expr_def(out << " ", p); + return out; + } + + void clause_proof::declare(std::ostream& out, expr* e) { + m_pp.collect(e); + m_pp.display_decls(out); + m.is_not(e, e); + m_pp.define_expr(out, e); + } + void clause_proof::update(status st, expr_ref_vector& v, proof* p) { TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";); if (ctx.get_fparams().m_clause_proof) m_trail.push_back(info(st, v, p)); if (m_on_clause_eh) m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data()); + if (m_pp_out) { + auto& out = *m_pp_out; + for (auto* e : v) + declare(out, e); + switch (st) { + case clause_proof::status::assumption: + display_literals(out << "(assume", v) << ")\n"; + break; + case clause_proof::status::lemma: + case clause_proof::status::th_lemma: + case clause_proof::status::th_assumption: + if (p) + declare(out, p); + display_hint(display_literals(out << "(infer", v), p) << ")\n"; + break; + case clause_proof::status::deleted: + display_literals(out << "(del", v) << ")\n"; + break; + default: + UNREACHABLE(); + } + } } void clause_proof::update(clause& c, status st, proof* p) { - if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + if (!is_enabled()) return; m_lits.reset(); for (literal lit : c) diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h index f15d0ffe0..42f283f1d 100644 --- a/src/smt/smt_clause_proof.h +++ b/src/smt/smt_clause_proof.h @@ -26,8 +26,10 @@ Revision History: --*/ #pragma once +#include "ast/ast_pp_util.h" #include "smt/smt_theory.h" #include "smt/smt_clause.h" +#include "smt/smt_justification.h" #include "tactic/user_propagator_base.h" namespace smt { @@ -55,13 +57,20 @@ namespace smt { ast_manager& m; expr_ref_vector m_lits; vector m_trail; - bool m_on_clause_active = false; + bool m_enabled = false; user_propagator::on_clause_eh_t m_on_clause_eh; void* m_on_clause_ctx = nullptr; + ast_pp_util m_pp; + scoped_ptr m_pp_out; + void update(status st, expr_ref_vector& v, proof* p); void update(clause& c, status st, proof* p); status kind2st(clause_kind k); proof* justification2proof(status st, justification* j); + void log(status st, proof* p); + void declare(std::ostream& out, expr* e); + std::ostream& display_literals(std::ostream& out, expr_ref_vector const& v); + std::ostream& display_hint(std::ostream& out, proof* p); public: clause_proof(context& ctx); void shrink(clause& c, unsigned new_size); @@ -69,13 +78,14 @@ namespace smt { void add(literal lit1, literal lit2, clause_kind k, justification* j); void add(clause& c); void add(unsigned n, literal const* lits, clause_kind k, justification* j); + void propagate(literal lit, justification const& j, literal_vector const& ante); void del(clause& c); proof_ref get_proof(bool inconsistent); - bool on_clause_active() const { return m_on_clause_active; } + bool is_enabled() const { return m_enabled; } void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) { m_on_clause_eh = on_clause; m_on_clause_ctx = ctx; - m_on_clause_active = !!m_on_clause_eh; + m_enabled |= !!m_on_clause_eh; } }; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 45ff1900d..d075c0652 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -350,6 +350,7 @@ namespace smt { literal_vector & antecedents = m_tmp_literal_vector; antecedents.reset(); justification2literals_core(js, antecedents); + m_ctx.get_clause_proof().propagate(consequent, *js, antecedents); for (literal l : antecedents) process_antecedent(l, num_marks); (void)consequent; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 84b4906ca..a8d2f268d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -284,7 +284,7 @@ namespace smt { TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_smt2(tout, l) << "\n"; tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n"; - /*display(tout, j);*/ + display(tout, j); ); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); @@ -639,7 +639,6 @@ namespace smt { if (val != l_true) { if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE) m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr()); - assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs))); } // It is not necessary to reinsert the equality to the congruence table @@ -1347,6 +1346,7 @@ namespace smt { TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v));); if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) { literal n_eq = literal(l.var(), true); + IF_VERBOSE(0, verbose_stream() << "eq-conflict @" << m_scope_lvl << "\n"); set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq); } } @@ -3732,6 +3732,7 @@ namespace smt { flet l(m_searching, true); TRACE("after_init_search", display(tout);); IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";); + log_stats(); TRACE("search_lite", tout << "searching...\n";); lbool status = l_undef; unsigned curr_lvl = m_scope_lvl; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 4a5f64926..2b3a343f7 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1706,7 +1706,9 @@ namespace smt { void get_units(expr_ref_vector& result); - bool on_clause_active() const { return m_clause_proof.on_clause_active(); } + bool clause_proof_active() const { return m_clause_proof.is_enabled(); } + + clause_proof& get_clause_proof() { return m_clause_proof; } void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) { m_clause_proof.register_on_clause(ctx, on_clause); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 63848418f..26e23d92d 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1593,7 +1593,7 @@ namespace smt { TRACE("gate_clause", tout << mk_ll_pp(pr, m);); mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); } - else if (m_clause_proof.on_clause_active()) { + else if (clause_proof_active()) { ptr_buffer new_lits; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; @@ -1638,7 +1638,7 @@ namespace smt { } mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); } - else if (pr && on_clause_active()) + else if (pr && clause_proof_active()) // support logging of quantifier instantiations and other more detailed information mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); else