From 50c855e2ebc715972b1fa8365a5e4c8fc66cda06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Apr 2023 16:32:16 -0700 Subject: [PATCH] count gcd conflicts, log row id in rows --- src/smt/theory_arith_pp.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index d10bfca55a2..b0d43bc00ac 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -37,6 +37,7 @@ namespace smt { st.update("arith assume eqs", m_stats.m_assume_eqs); st.update("arith offset eqs", m_stats.m_offset_eqs); st.update("arith gcd tests", m_stats.m_gcd_tests); + st.update("arith gcd conflicts", m_stats.m_gcd_conflicts); st.update("arith ineq splits", m_stats.m_branches); st.update("arith gomory cuts", m_stats.m_gomory_cuts); st.update("arith branch int", m_stats.m_branch_infeasible_int); @@ -82,8 +83,9 @@ namespace smt { template void theory_arith::display_row(std::ostream & out, row const & r, bool compact) const { - - out << "(v" << r.get_base_var() << ") : "; + + column const & c = m_columns[r.get_base_var()]; + out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : "; bool first = true; for (auto const& e : r) { if (!e.is_dead()) {