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

call normalize_e_by_gcd() only when moving an entry from F to S

Browse source
This commit is contained in:
Lev Nachmanson 2025-02-04 12:38:16 -10:00 committed by Lev Nachmanson
parent 99538567a7
commit 0bf3ca87e7
1 changed files with 30 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1075,7 +1075,12 @@ namespace lp {
}
template <typename K>
mpq gcd_of_coeffs(const K& k) {
mpq gcd_of_coeffs(const K& k, bool check_for_one) {
if (check_for_one)
for (const auto& p : k)
if (p.coeff().is_one() || p.coeff().is_minus_one())
return mpq(1);
mpq g(0);
for (const auto& p : k) {
SASSERT(p.coeff().is_int());
@ -1125,10 +1130,10 @@ namespace lp {
// If there is no conflict the entry is divided, normalized, by gcd.
// The function returns true if and only if there is no conflict. In the case of a conflict a branch
// can be returned as well.
bool normalize_e_by_gcd(unsigned ei) {
bool normalize_e_by_gcd(unsigned ei, mpq& g) {
mpq & e = m_sum_of_fixed[ei];
TRACE("dioph_eq", print_entry(ei, tout) << std::endl;);
mpq g = gcd_of_coeffs(m_e_matrix.m_rows[ei]);
g = gcd_of_coeffs(m_e_matrix.m_rows[ei], false);
if (g.is_zero() || g.is_one()) {
SASSERT(g.is_one() || e.is_zero());
return true;
@ -1159,20 +1164,6 @@ namespace lp {
return false;
}
// iterate over F: return true if no conflict is found and false otherwise
bool normalize_by_gcd() {
for (unsigned l = 0; l < m_e_matrix.row_count(); l++) {
if (!belongs_to_f(l)) continue;
if (!normalize_e_by_gcd(l)) {
SASSERT(entry_invariant(l));
m_conflict_index = l;
return false;
}
SASSERT(entry_invariant(l));
}
return true;
}
void init_term_from_constraint(term_o& t, const lar_base_constraint& c) {
for (const auto& p : c.coeffs()) {
t.add_monomial(p.first, p.second);
@ -1438,7 +1429,7 @@ namespace lp {
SASSERT(
fix_vars(term_to_tighten + open_ml(m_term_with_index.to_term())) ==
term_to_lar_solver(remove_fresh_vars(create_term_from_ind_c())));
mpq g = gcd_of_coeffs(m_indexed_work_vector);
mpq g = gcd_of_coeffs(m_indexed_work_vector, true);
TRACE("dioph_eq", tout << "after process_q_with_S\nt:";
print_term_o(create_term_from_ind_c(), tout) << std::endl;
tout << "g:" << g << std::endl;
@ -1578,24 +1569,11 @@ namespace lp {
}
lia_move process_f() {
bool progress = true;
while (progress) {
if (!normalize_by_gcd()) {
if (m_report_branch) {
lra.stats().m_dio_branch_from_proofs++;
m_report_branch = false;
return lia_move::branch;
} else {
lra.stats().m_dio_normalize_conflicts++;
}
return lia_move::conflict;
}
progress = rewrite_eqs();
while (rewrite_eqs()) {}
if (m_conflict_index != UINT_MAX) {
lra.stats().m_dio_rewrite_conflicts++;
return lia_move::conflict;
}
}
return lia_move::undef;
}
@ -1956,7 +1934,7 @@ namespace lp {
return ret;
}
SASSERT(ret == lia_move::undef);
m_max_number_of_iterations = std::max((unsigned)5, (unsigned)m_max_number_of_iterations/2);
m_max_number_of_iterations = (unsigned)m_max_number_of_iterations/2;
return lia_move::undef;
}
@ -2336,6 +2314,7 @@ namespace lp {
return false;
}
}
auto [ahk, k, k_sign] = find_minimal_abs_coeff(ei);
if (ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_entry(ei, tout););
@ -2343,6 +2322,20 @@ namespace lp {
eliminate_var_in_f(ei, k, k_sign);
return true;
}
mpq gcd;
if (!normalize_e_by_gcd(ei, gcd)) {
m_conflict_index = ei;
return false;
}
if (!gcd.is_one()){
ahk /= gcd;
if (ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_entry(ei, tout););
move_entry_from_f_to_s(k, ei);
eliminate_var_in_f(ei, k, k_sign);
return true;
}
}
if (n == 0 || the_smallest_ahk > ahk) {
n = 1;
@ -2358,7 +2351,7 @@ namespace lp {
kh_sign = k_sign;
}
}
if (h == -1) return false;
if (h == UINT_MAX) return false;
SASSERT(!the_smallest_ahk.is_one());
fresh_var_step(h, kh, the_smallest_ahk * mpq(kh_sign));
return true;