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 stats on m_dio_branching_conflicts

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-05 10:38:51 -10:00 committed by Lev Nachmanson
parent 0bf3ca87e7
commit 7e02dfe484
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/dioph_eq.cpp
View file

@ -1733,6 +1733,7 @@ namespace lp {
if (m_branch_stack.size() == 0) { if (m_branch_stack.size() == 0) {
lra.stats().m_dio_branching_infeasibles++; lra.stats().m_dio_branching_infeasibles++;
transfer_explanations_from_closed_branches(); transfer_explanations_from_closed_branches();
lra.stats().m_dio_branching_conflicts++;
return lia_move::conflict; return lia_move::conflict;
} }
need_create_branch = false; need_create_branch = false;
@ -1761,6 +1762,7 @@ namespace lp {
if (m_branch_stack.size() == 0) { if (m_branch_stack.size() == 0) {
lra.stats().m_dio_branching_infeasibles++; lra.stats().m_dio_branching_infeasibles++;
transfer_explanations_from_closed_branches(); transfer_explanations_from_closed_branches();
lra.stats().m_dio_branching_conflicts++;
return lia_move::conflict; return lia_move::conflict;
} }
TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl; TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;

2
src/math/lp/lp_settings.h
View file

@ -137,6 +137,7 @@ struct statistics {
unsigned m_dio_branching_infeasibles = 0; unsigned m_dio_branching_infeasibles = 0;
unsigned m_dio_rewrite_conflicts = 0; unsigned m_dio_rewrite_conflicts = 0;
unsigned m_dio_branching_sats = 0; unsigned m_dio_branching_sats = 0;
unsigned m_dio_branching_conflicts = 0;
::statistics m_st = {}; ::statistics m_st = {};
void reset() { void reset() {
@ -179,6 +180,7 @@ struct statistics {
st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts); st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
st.update("arith-dio-branching-sats", m_dio_branching_sats); st.update("arith-dio-branching-sats", m_dio_branching_sats);
st.update("arith-dio-branching-depth", m_dio_branching_depth); st.update("arith-dio-branching-depth", m_dio_branching_depth);
st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts);
st.copy(m_st); st.copy(m_st);
} }
}; };