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

add logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-16 14:48:19 -07:00
parent 7fdcbbaee9
commit 99b606b861
2 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith_core.h
View file

@ -3097,6 +3097,8 @@ namespace smt {
m_stats.m_conflicts++; m_stats.m_conflicts++;
m_num_conflicts++; m_num_conflicts++;
TRACE("arith_conflict", TRACE("arith_conflict",
if (proof_rule)
tout << proof_rule << "\n";
tout << "scope: " << ctx.get_scope_level() << "\n"; tout << "scope: " << ctx.get_scope_level() << "\n";
for (unsigned i = 0; i < num_literals; i++) { for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]); ctx.display_detailed_literal(tout, lits[i]);

12
src/smt/theory_lra.cpp
View file

@ -3159,11 +3159,15 @@ public:
// lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed // lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
++m_num_conflicts; ++m_num_conflicts;
++m_stats.m_conflicts; ++m_stats.m_conflicts;
TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); ); TRACE("arith",
TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n");); tout << "lemma scope: " << ctx().get_scope_level();
for (auto ev : m_explanation) { for (auto const& p : m_params) tout << " " << p;
tout << "\n";
display_evidence(tout, m_explanation);
display(tout << "is-conflict: " << is_conflict << "\n"););
for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs); set_evidence(ev.ci(), m_core, m_eqs);
}
// SASSERT(validate_conflict(m_core, m_eqs)); // SASSERT(validate_conflict(m_core, m_eqs));
dump_conflict(m_core, m_eqs); dump_conflict(m_core, m_eqs);
if (is_conflict) { if (is_conflict) {