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

more accurate work with Markovich number

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-09 07:53:55 -08:00 committed by Lev Nachmanson
parent bdb8f54150
commit 2131e9b4e4
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1999,8 +1999,8 @@ namespace lp {
} }
} }
unsigned find_markovich_number(unsigned k, unsigned h) { unsigned get_markovich_number(unsigned k, unsigned h) {
return m_e_matrix.m_columns[k].size() * m_e_matrix.m_rows[h].size(); return (m_e_matrix.m_columns[k].size() - 1) * (m_e_matrix.m_rows[h].size() - 1);
} }
std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) { std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) {
@ -2021,7 +2021,7 @@ namespace lp {
} }
} }
return std::make_tuple(ahk, k, k_sign, find_markovich_number(k, ei)); return std::make_tuple(ahk, k, k_sign, get_markovich_number(k, ei));
} }
@ -2354,7 +2354,7 @@ namespace lp {
return false; return false;
unsigned h = -1; unsigned h = -1;
unsigned n = 0; // number of choices for a fresh variable unsigned n = 0; // number of choices for a fresh variable
mpq the_smallest_ahk; mpq min_ahk;
unsigned kh; unsigned kh;
int kh_sign; int kh_sign;
unsigned h_markovich_number; unsigned h_markovich_number;
@ -2380,27 +2380,29 @@ namespace lp {
if (!gcd.is_one()) if (!gcd.is_one())
ahk /= gcd; ahk /= gcd;
if (n == 0 || the_smallest_ahk > ahk) { if (n == 0 || min_ahk > ahk) {
ih = i; ih = i;
n = 1; n = 1;
the_smallest_ahk = ahk; min_ahk = ahk;
h = ei; h = ei;
kh = k; kh = k;
kh_sign = k_sign; kh_sign = k_sign;
h_markovich_number = markovich_number; h_markovich_number = markovich_number;
continue; continue;
} }
if (the_smallest_ahk == ahk && h_markovich_number > markovich_number) { if (min_ahk == ahk && h_markovich_number > markovich_number) {
ih = i; ih = i;
h = ei; h = ei;
kh = k; kh = k;
kh_sign = k_sign; kh_sign = k_sign;
h_markovich_number = markovich_number; h_markovich_number = markovich_number;
} }
if (min_ahk.is_one() && h_markovich_number == 0)
break;
} }
if (h == UINT_MAX) return false; if (h == UINT_MAX) return false;
SASSERT(h == f_vector[ih]); SASSERT(h == f_vector[ih]);
if (the_smallest_ahk.is_one()) { if (min_ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout);); TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout););
move_entry_from_f_to_s(kh, h); move_entry_from_f_to_s(kh, h);
eliminate_var_in_f(h, kh, kh_sign); eliminate_var_in_f(h, kh, kh_sign);
@ -2409,7 +2411,7 @@ namespace lp {
} }
f_vector.pop_back(); f_vector.pop_back();
} else } else
fresh_var_step(h, kh, the_smallest_ahk * mpq(kh_sign)); fresh_var_step(h, kh, min_ahk * mpq(kh_sign));
return true; return true;
} }