mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-01 14:57:57 +00:00
Code Activity

- When removing a fresh var xt, collect all fresh defs that transitively reference it

Browse source 
- Remove them all from m_fresh_k2xt_terms and m_row2fresh_defs
    - Mark rows containing those vars in m_changed_rows for recalculation
    - Move remove_irrelevant_fresh_defs() before the recalculate loop so all affected rows get recalculated

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-29 06:17:14 -10:00
parent 1ec30620ef
commit adac953e87
1 changed files with 91 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -752,6 +752,7 @@ namespace lp {
m_var_register.shrink(m_e_matrix.column_count());
remove_out_of_bounds_fresh_defs();
remove_irrelevant_fresh_defs_for_row(i);
if (m_k2s.has_val(i))
@ -907,7 +908,6 @@ namespace lp {
return;
}
substitute_on_q(ei);
SASSERT(entry_invariant(ei));
}
void substitute_on_q_with_entry_in_S(unsigned ei, unsigned j, const mpq& alpha) {
@ -1016,17 +1016,86 @@ namespace lp {
}
}
void remove_irrelevant_fresh_defs_for_row(unsigned ei) {
auto it = m_row2fresh_defs.find(ei);
if (it == m_row2fresh_defs.end()) return;
for (unsigned xt : it->second) {
if (m_fresh_k2xt_terms.has_second_key(xt))
m_fresh_k2xt_terms.erase_by_second_key(xt);
}
m_row2fresh_defs.erase(it);
// Remove fresh definitions whose terms reference the given variable
// Mark rows containing stale fresh variable for recalculation
void handle_stale_var_in_matrix(unsigned xt) {
if (xt >= m_e_matrix.column_count())
return;
// Mark all rows containing xt for recalculation
for (const auto& cell : m_e_matrix.m_columns[xt])
m_changed_rows.insert(cell.var());
}
void remove_irrelevant_fresh_defs() {
// Collect all fresh vars that directly or transitively reference removed_xt
void collect_dependent_fresh_vars(unsigned removed_xt, std_vector<unsigned>& to_remove) {
std_vector<unsigned> newly_found;
for (const auto& p : m_fresh_k2xt_terms.m_bij.key_val_pairs()) {
unsigned xt = p.second;
if (xt == removed_xt) continue;
if (std::find(to_remove.begin(), to_remove.end(), xt) != to_remove.end())
continue; // already marked for removal
const lar_term& term = m_fresh_k2xt_terms.get_by_val(xt).first;
// Check if term contains removed_xt or any var already marked for removal
if (term.contains(removed_xt)) {
newly_found.push_back(xt);
} else {
for (unsigned marked : to_remove)
if (term.contains(marked)) {
newly_found.push_back(xt);
break;
}
}
}
for (unsigned xt : newly_found)
to_remove.push_back(xt);
// Recurse if we found new ones (they might have dependents too)
if (!newly_found.empty())
for (unsigned xt : newly_found)
collect_dependent_fresh_vars(xt, to_remove);
}
// Deep clean: remove fresh var and all dependents, clean m_e_matrix
void deep_remove_fresh_var(unsigned removed_xt) {
if (!m_fresh_k2xt_terms.has_second_key(removed_xt))
return;
// Collect all vars that need to be removed (removed_xt and its dependents)
std_vector<unsigned> to_remove;
to_remove.push_back(removed_xt);
collect_dependent_fresh_vars(removed_xt, to_remove);
// Remove them all
for (unsigned xt : to_remove) {
if (!m_fresh_k2xt_terms.has_second_key(xt))
continue;
// Get the row before erasing
unsigned row = m_fresh_k2xt_terms.get_by_val(xt).second;
m_fresh_k2xt_terms.erase_by_second_key(xt);
// Update m_row2fresh_defs
auto it = m_row2fresh_defs.find(row);
if (it != m_row2fresh_defs.end()) {
it->second.erase(std::remove(it->second.begin(), it->second.end(), xt), it->second.end());
if (it->second.empty())
m_row2fresh_defs.erase(it);
}
// Mark rows containing xt for recalculation
handle_stale_var_in_matrix(xt);
}
}
void remove_irrelevant_fresh_defs_for_row(unsigned ei) {
auto it = m_row2fresh_defs.find(ei);
if (it == m_row2fresh_defs.end()) return;
// Copy the list since deep_remove_fresh_var modifies m_row2fresh_defs
std_vector<unsigned> xts_to_remove = it->second;
for (unsigned xt : xts_to_remove)
deep_remove_fresh_var(xt);
// Ensure the row entry is removed (might already be gone)
m_row2fresh_defs.erase(ei);
}
// Remove fresh definitions for columns that are out of bounds after shrinking
void remove_out_of_bounds_fresh_defs() {
std_vector<unsigned> xt_to_remove;
std_vector<unsigned> rows_to_remove_the_defs_from;
for (const auto& p : m_fresh_k2xt_terms.m_bij.key_val_pairs()) {
@ -1037,17 +1106,18 @@ namespace lp {
}
}
for (unsigned xt : xt_to_remove) {
m_fresh_k2xt_terms.erase_by_second_key(xt);
}
for (unsigned xt : xt_to_remove)
deep_remove_fresh_var(xt);
for (unsigned ei : m_changed_rows) {
for (unsigned ei : rows_to_remove_the_defs_from)
remove_irrelevant_fresh_defs_for_row(ei);
}
}
for (unsigned ei : rows_to_remove_the_defs_from) {
void remove_irrelevant_fresh_defs() {
remove_out_of_bounds_fresh_defs();
for (unsigned ei : m_changed_rows)
remove_irrelevant_fresh_defs_for_row(ei);
}
}
// this is a non-const function - it can set m_some_terms_are_ignored to true
@ -1089,6 +1159,9 @@ namespace lp {
for (unsigned ei : more_changed_rows)
m_changed_rows.insert(ei);
// Remove irrelevant fresh defs first - this may add more rows to m_changed_rows
remove_irrelevant_fresh_defs();
for (unsigned ei : m_changed_rows) {
if (ei >= m_e_matrix.row_count())
continue;
@ -1100,11 +1173,11 @@ namespace lp {
if (!m_e_matrix.m_columns.empty() && m_e_matrix.m_columns.back().size() == 0) {
m_e_matrix.m_columns.pop_back();
m_var_register.shrink(m_e_matrix.column_count());
remove_out_of_bounds_fresh_defs();
}
if (!m_l_matrix.m_columns.empty() && m_l_matrix.m_columns.back().size() == 0)
m_l_matrix.m_columns.pop_back();
}
remove_irrelevant_fresh_defs();
eliminate_substituted_in_changed_rows();
m_changed_f_columns.reset();
m_changed_rows.reset();