add stats on m_dio_branching_conflicts

Signed-off-by: Lev Nachmanson <[email protected]>
Z3Prover · Feb 11, 2025 · 7e02dfe · 7e02dfe
1 parent 0bf3ca8
commit 7e02dfe
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git 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
@@ -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);
     }
 };