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

handle empty rows in m_e_matrix

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-10-15 08:01:20 -07:00 committed by Lev Nachmanson
parent ba7268c895
commit 0f03e7560d
1 changed files with 31 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -561,6 +561,10 @@ public:
return lia_move::conflict; return lia_move::conflict;
} }
rewrite_eqs(); rewrite_eqs();
if (m_conflict_index != -1) {
lra.settings().stats().m_dio_conflicts++;
return lia_move::conflict;
}
} }
TRACE("dioph_eq", print_S(tout);); TRACE("dioph_eq", print_S(tout););
// lia_move ret = tighten_with_S(); // lia_move ret = tighten_with_S();
@ -756,31 +760,45 @@ public:
} }
// k is the index of the index of the variable with the coefficient +-1 that is being substituted // k is the index of the index of the variable with the coefficient +-1 that is being substituted
void move_entry_from_f_to_s(unsigned k, std::list<unsigned>::iterator it) { void move_entry_from_f_to_s(unsigned k, unsigned h) {
SASSERT(m_eprime[*it].m_entry_status == entry_status::F); SASSERT(m_eprime[h].m_entry_status == entry_status::F);
m_eprime[*it].m_entry_status = entry_status::S; m_eprime[h].m_entry_status = entry_status::S;
if (k >= m_k2s.size()) { // k is a fresh variable if (k >= m_k2s.size()) { // k is a fresh variable
m_k2s.resize(k+1, -1 ); m_k2s.resize(k+1, -1 );
} }
m_s.push_back(*it); m_s.push_back(h);
TRACE("dioph_eq", tout << "removed " << *it << "th entry from F" << std::endl;); TRACE("dioph_eq", tout << "removed " << h << "th entry from F" << std::endl;);
m_k2s[k] = *it; m_k2s[k] = h;
m_f.erase(it); m_f.remove(h);
} }
// this is the step 6 or 7 of the algorithm // this is the step 6 or 7 of the algorithm
void rewrite_eqs() { void rewrite_eqs() {
auto eh_it = pick_eh(); unsigned h = -1;
auto& eprime_entry = m_eprime[*eh_it]; auto it = m_f.begin();
TRACE("dioph_eq", print_eprime_entry(*eh_it, tout);); while (it != m_f.end()) {
if (m_e_matrix.m_rows[m_eprime[*it].m_row_index].size() == 0)
if (m_eprime[*it].m_c.is_zero()) {
it = m_f.erase(it);
continue;
} else {
m_conflict_index = *it;
return;
}
h = *it;
break;
}
if (h == -1) return;
auto& eprime_entry = m_eprime[h];
TRACE("dioph_eq", print_eprime_entry(h, tout););
auto [ahk, k, k_sign] = find_minimal_abs_coeff(eprime_entry.m_row_index); auto [ahk, k, k_sign] = find_minimal_abs_coeff(eprime_entry.m_row_index);
TRACE("dioph_eq", tout << "ahk:" << ahk << ", k:" << k << ", k_sign:" << k_sign << std::endl;); TRACE("dioph_eq", tout << "ahk:" << ahk << ", k:" << k << ", k_sign:" << k_sign << std::endl;);
if (ahk.is_one()) { if (ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_eprime_entry(*eh_it, tout);); TRACE("dioph_eq", tout << "push to S:\n"; print_eprime_entry(h, tout););
move_entry_from_f_to_s(k, eh_it); move_entry_from_f_to_s(k, h);
eliminate_var_in_f(eprime_entry, k , k_sign); eliminate_var_in_f(eprime_entry, k , k_sign);
} else { } else {
fresh_var_step(*eh_it, k, ahk*mpq(k_sign)); fresh_var_step(h, k, ahk*mpq(k_sign));
} }
} }
public: public: