mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

wip - features and bug-fixes to proof logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-18 07:54:49 -07:00
parent 3bf1b606df
commit 7b3a634b8d
11 changed files with 45 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_egraph.cpp
View file

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

14
src/sat/sat_solver.cpp
View file

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

2
src/sat/smt/distinct_theory_checker.h
View file

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

2
src/sat/smt/euf_internalize.cpp
View file

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

17
src/sat/smt/euf_proof.cpp
View file

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

18
src/sat/smt/euf_proof_checker.cpp
View file

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

5
src/sat/smt/euf_proof_checker.h
View file

@ -90,8 +90,9 @@ namespace euf {
bool m_check_rup = false;
// for logging
symbol m_last_rule;
unsigned m_num_last_rules = 0;
map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_hint2hit;
unsigned m_num_logs = 0;
void add_units() {
auto const& units = m_drat.units();

15
src/sat/smt/euf_solver.cpp
View file

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

9
src/sat/smt/euf_solver.h
View file

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

2
src/sat/smt/sat_th.cpp
View file

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

2
src/sat/smt/sat_th.h
View file

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