mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add logging of propagations to smt core

Browse source 
log theory propagations with annotation "smt".
It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core.
This commit is contained in:
Nikolaj Bjorner 2022-11-23 08:01:15 +07:00
parent 5374142e3e
commit 6188c536ef
7 changed files with 95 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/qi_queue.cpp
View file

@ -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);

80
src/smt/smt_clause_proof.cpp
View file

@ -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)

16
src/smt/smt_clause_proof.h
View file

@ -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<info> 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<std::ofstream> 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;
}
};

1
src/smt/smt_conflict_resolution.cpp
View file

@ -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;

5
src/smt/smt_context.cpp
View file

@ -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<bool> 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;

4
src/smt/smt_context.h
View file

@ -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);

4
src/smt/smt_internalizer.cpp
View file

@ -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<expr> 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