mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

try markovich number

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-07 22:39:52 -08:00 committed by Lev Nachmanson
parent cec8dc2e6e
commit f2c1fd4c14
1 changed files with 4 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1999,13 +1999,8 @@ namespace lp {
} }
} }
unsigned find_markovich_number(unsigned k, unsigned h) {
unsigned find_markovich_number(unsigned k) { return m_e_matrix.m_columns[k].size() * m_e_matrix.m_rows[h].size();
unsigned r = 0;
for (const auto & p: m_e_matrix.m_columns[k]) {
r += m_e_matrix.m_rows[p.var()].size();
}
return r;
} }
std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) { std::tuple<mpq, unsigned, int, unsigned> 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 get_term_to_subst(const term_o& eh, unsigned k, int k_sign) {
term_o t; term_o t;
for (const auto& p : eh) { for (const auto& p : eh) {