mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
wip - proof logging fixes
This commit is contained in:
parent
1fc77c8c00
commit
f0b85716a9
|
@ -159,6 +159,9 @@ namespace euf {
|
|||
v = si.add_bool_var(e);
|
||||
s().set_external(v);
|
||||
s().set_eliminated(v, false);
|
||||
m_bool_var2expr.reserve(v + 1, nullptr);
|
||||
m_bool_var2expr[v] = e;
|
||||
m_var_trail.push_back(v);
|
||||
sat::literal lit2 = literal(v, false);
|
||||
th_proof_hint* ph1 = nullptr, * ph2 = nullptr;
|
||||
if (use_drat()) {
|
||||
|
|
|
@ -391,15 +391,23 @@ namespace euf {
|
|||
}
|
||||
|
||||
|
||||
void smt_proof_checker::log_verified(app* proof_hint) {
|
||||
void smt_proof_checker::log_verified(app* proof_hint, bool success) {
|
||||
if (!proof_hint)
|
||||
return;
|
||||
|
||||
symbol n = proof_hint->get_name();
|
||||
m_hint2hit.insert_if_not_there(n, 0)++;
|
||||
if (success)
|
||||
m_hint2hit.insert_if_not_there(n, 0)++;
|
||||
else
|
||||
m_hint2miss.insert_if_not_there(n, 0)++;
|
||||
++m_num_logs;
|
||||
|
||||
if (m_num_logs < 100 || (m_num_logs % 1000) == 0) {
|
||||
std::cout << "(verified";
|
||||
std::cout << "(proofs";
|
||||
for (auto const& [k, v] : m_hint2hit)
|
||||
std::cout << " :" << k << " " << v;
|
||||
std::cout << " +" << k << " " << v;
|
||||
for (auto const& [k, v] : m_hint2miss)
|
||||
std::cout << " -" << k << " " << v;
|
||||
std::cout << ")\n";
|
||||
}
|
||||
}
|
||||
|
@ -424,7 +432,7 @@ namespace euf {
|
|||
|
||||
if (is_rup(proof_hint) && check_rup(clause)) {
|
||||
if (m_check_rup) {
|
||||
log_verified(proof_hint);
|
||||
log_verified(proof_hint, true);
|
||||
add_clause(clause);
|
||||
}
|
||||
return;
|
||||
|
@ -440,7 +448,7 @@ namespace euf {
|
|||
}
|
||||
}
|
||||
if (units_are_rup) {
|
||||
log_verified(proof_hint);
|
||||
log_verified(proof_hint, true);
|
||||
add_clause(clause);
|
||||
return;
|
||||
}
|
||||
|
@ -454,11 +462,13 @@ namespace euf {
|
|||
// The VC function is a no-op if the proof hint does not have an associated vc generator.
|
||||
expr_ref_vector vc(clause);
|
||||
if (m_checker.vc(proof_hint, clause, vc)) {
|
||||
log_verified(proof_hint);
|
||||
log_verified(proof_hint, true);
|
||||
add_clause(clause);
|
||||
return;
|
||||
}
|
||||
|
||||
log_verified(proof_hint, false);
|
||||
|
||||
ensure_solver();
|
||||
m_solver->push();
|
||||
for (expr* lit : vc)
|
||||
|
|
|
@ -89,7 +89,7 @@ namespace euf {
|
|||
|
||||
// for logging
|
||||
|
||||
map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_hint2hit;
|
||||
map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_hint2hit, m_hint2miss;
|
||||
unsigned m_num_logs = 0;
|
||||
|
||||
void add_units() {
|
||||
|
@ -98,7 +98,7 @@ namespace euf {
|
|||
m_units.push_back(units[i].first);
|
||||
}
|
||||
|
||||
void log_verified(app* proof_hint);
|
||||
void log_verified(app* proof_hint, bool success);
|
||||
|
||||
void diagnose_rup_failure(expr_ref_vector const& clause);
|
||||
|
||||
|
|
Loading…
Reference in a new issue