mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

cleanup

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-01-01 11:21:16 -10:00 • committed by Lev Nachmanson
parent ceeece6770
commit a0ece6dd2c
1 changed files with 3 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -464,9 +464,9 @@ namespace lp {
std_vector<unsigned> fresh_entries_to_remove;
for (unsigned j = 0; j < m_fresh_definitions.size(); j++) {
unsigned k = m_fresh_definitions[j];
if (k == -1) continue;
if (k == UINT_MAX) continue;
for (const auto & p: m_e_matrix.m_rows[k]) {
if (contains(m_changed_columns, p.var()) || contains(m_changed_columns,p.var())) {
if (contains(m_changed_columns, p.var())) {
fresh_entries_to_remove.push_back(k);
continue;
}
@ -484,7 +484,6 @@ namespace lp {
NOT_IMPLEMENTED_YET();
}
for (unsigned j : m_changed_columns) {
if (!m_var_register.external_is_used(j)) continue;
for (unsigned k : m_columns_to_terms[j]) {
changed_terms.insert(k);
}
@ -495,11 +494,6 @@ namespace lp {
entries_to_recalculate.insert(p.var());
}
}
for (unsigned j : m_changed_columns) {
for (unsigned k : m_columns_to_terms[j]) {
changed_terms.insert(k);
}
}
for (unsigned j : changed_terms) {
for (const auto & cs: m_l_matrix.column(j)) {
TRACE("dioph_eq", tout << "insert into entries_to_recalculate " << cs.var() << " for changed_term j=" << j<< std::endl;);
@ -524,7 +518,7 @@ namespace lp {
else it++;
}
for (unsigned k = 0; k < m_k2s.size(); k++) {
if (m_k2s[k] != -1 && contains(entries_to_recalculate, m_k2s[k])) {
if (m_k2s[k] != UINT_MAX && contains(entries_to_recalculate, m_k2s[k])) {
m_k2s[k] = -1;
}
}