From a0ece6dd2c9b72553fc27de3587eac74f0d36a15 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 1 Jan 2025 11:21:16 -1000
Subject: [PATCH] cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/dioph_eq.cpp | 12 +++---------
1 file changed, 3 insertions(+), 9 deletions(-)
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 9366f324c..f7d35ee91 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -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;
}
}