mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +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
parent 07a1a880f2
commit 86e39f3140
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 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<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 t;
for (const auto& p : eh) {