From f2c1fd4c140e6df8682952e08e7f4ebdad9d5948 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 7 Feb 2025 22:39:52 -0800 Subject: [PATCH] try markovich number Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 8a5e61c5e..2f5936c22 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1999,13 +1999,8 @@ namespace lp { } } - - unsigned find_markovich_number(unsigned k) { - unsigned r = 0; - for (const auto & p: m_e_matrix.m_columns[k]) { - r += m_e_matrix.m_rows[p.var()].size(); - } - return r; + unsigned find_markovich_number(unsigned k, unsigned h) { + return m_e_matrix.m_columns[k].size() * m_e_matrix.m_rows[h].size(); } std::tuple find_minimal_abs_coeff(unsigned ei) { @@ -2026,9 +2021,10 @@ namespace lp { } } - return std::make_tuple(ahk, k, k_sign, find_markovich_number(k)); + return std::make_tuple(ahk, k, k_sign, find_markovich_number(k, ei)); } + term_o get_term_to_subst(const term_o& eh, unsigned k, int k_sign) { term_o t; for (const auto& p : eh) {