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

ignore large changed_columns

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-06 05:45:50 -10:00 committed by Lev Nachmanson
parent 3ac11cd136
commit bd8cf29df7
1 changed files with 2 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -883,14 +883,7 @@ namespace lp {
return lia.column_is_int(term.j()); return lia.column_is_int(term.j());
} }
void delete_column(unsigned j) {
SASSERT(j >= m_e_matrix.column_count());
SASSERT(m_k2s.has_key(j) == false);
SASSERT(m_k2s.has_val(j) == false);
SASSERT(m_columns_to_terms.find(j) == m_columns_to_terms.end());
}
void clear_e_row(unsigned ei) { void clear_e_row(unsigned ei) {
auto & row = m_e_matrix.m_rows[ei]; auto & row = m_e_matrix.m_rows[ei];
while (row.size() > 0) { while (row.size() > 0) {
@ -958,11 +951,7 @@ namespace lp {
} }
void process_changed_columns() { void process_changed_columns() {
for (unsigned j : m_changed_columns) {
if (j >= this->lra.column_count()) {
delete_column(j);
}
}
find_changed_terms_and_more_changed_rows(); find_changed_terms_and_more_changed_rows();
for (unsigned j : m_changed_terms) { for (unsigned j : m_changed_terms) {
if (j >= m_l_matrix.column_count()) continue; if (j >= m_l_matrix.column_count()) continue;