From 7e02dfe484c24008c1f8022891a401af376a2455 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 5 Feb 2025 10:38:51 -1000 Subject: [PATCH] add stats on m_dio_branching_conflicts Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 2 ++ src/math/lp/lp_settings.h | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 3d97e58f45..9d7ee09f1c 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1733,6 +1733,7 @@ namespace lp { if (m_branch_stack.size() == 0) { lra.stats().m_dio_branching_infeasibles++; transfer_explanations_from_closed_branches(); + lra.stats().m_dio_branching_conflicts++; return lia_move::conflict; } need_create_branch = false; @@ -1761,6 +1762,7 @@ namespace lp { if (m_branch_stack.size() == 0) { lra.stats().m_dio_branching_infeasibles++; transfer_explanations_from_closed_branches(); + lra.stats().m_dio_branching_conflicts++; return lia_move::conflict; } TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl; diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 77e0871e89..db94d1bf4d 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -137,6 +137,7 @@ struct statistics { unsigned m_dio_branching_infeasibles = 0; unsigned m_dio_rewrite_conflicts = 0; unsigned m_dio_branching_sats = 0; + unsigned m_dio_branching_conflicts = 0; ::statistics m_st = {}; void reset() { @@ -179,6 +180,7 @@ struct statistics { 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-depth", m_dio_branching_depth); + st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts); st.copy(m_st); } };