mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

fix a bug in tracking the changes in dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-09 15:56:44 -07:00 • committed by Lev Nachmanson
parent d289495ca4
commit 1131d5294d
1 changed files with 51 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -783,18 +783,20 @@ namespace lp {
std_vector<variable_branch_stats> m_branch_stats; std_vector<variable_branch_stats> m_branch_stats;
std_vector<branch> m_branch_stack; std_vector<branch> m_branch_stack;
std_vector<constraint_index> m_explanation_of_branches; std_vector<constraint_index> m_explanation_of_branches;
bool term_has_big_number(const lar_term& t) const { // it is a non-const function : it can set m_some_terms_are_ignored to true
bool term_has_big_number(const lar_term& t) {
for (const auto& p : t) { for (const auto& p : t) {
if (p.coeff().is_big()) if (abs(p.coeff()) > mpq(5) || p.coeff().is_big() || (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())) {
return true; m_some_terms_are_ignored = true;
if (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())
return true; return true;
} }
}
return false; return false;
} }
bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); } bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); }
// we add all terms, even those with big numbers, but we might choose to non process the latter.
void add_term_callback(const lar_term* t) { void add_term_callback(const lar_term* t) {
unsigned j = t->j(); unsigned j = t->j();
TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;); TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
@ -803,14 +805,7 @@ namespace lp {
m_some_terms_are_ignored = true; m_some_terms_are_ignored = true;
return; return;
} }
CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;); CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;);
if (ignore_big_nums() && term_has_big_number(*t)) {
TRACE("dio", tout << "term_has_big_number\n";);
m_some_terms_are_ignored = true;
return;
}
m_added_terms.push_back(t); m_added_terms.push_back(t);
mark_term_change(t->j()); mark_term_change(t->j());
auto undo = undo_add_term(*this, t); auto undo = undo_add_term(*this, t);
@ -825,13 +820,10 @@ namespace lp {
void update_column_bound_callback(unsigned j) { void update_column_bound_callback(unsigned j) {
if (!lra.column_is_int(j)) if (!lra.column_is_int(j))
return; return;
if (lra.column_has_term(j) && if (lra.column_has_term(j))
ignore_big_nums() && !term_has_big_number(lra.get_term(j)))
m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term
if (!lra.column_is_fixed(j)) if (!lra.column_is_fixed(j))
return; return;
if (ignore_big_nums() && lra.get_lower_bound(j).x.is_big())
return;
TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout););
m_changed_f_columns.insert(j); m_changed_f_columns.insert(j);
lra.trail().push(undo_fixed_column(*this, j)); lra.trail().push(undo_fixed_column(*this, j));
@ -861,7 +853,7 @@ namespace lp {
} }
void register_columns_to_term(const lar_term& t) { void register_columns_to_term(const lar_term& t) {
TRACE("dio_reg", tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;); CTRACE("dio_reg", t.j() == 1337, tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;);
for (const auto& p : t.ext_coeffs()) { for (const auto& p : t.ext_coeffs()) {
auto it = m_columns_to_terms.find(p.var()); auto it = m_columns_to_terms.find(p.var());
TRACE("dio_reg", tout << "register p.var():" << p.var() << "->" << t.j() << std::endl;); TRACE("dio_reg", tout << "register p.var():" << p.var() << "->" << t.j() << std::endl;);
@ -1062,21 +1054,29 @@ namespace lp {
} }
} }
void process_changed_columns(std_vector<unsigned> &f_vector) { // this is a non-const function - it can set m_some_terms_are_ignored to true
bool is_big_term_or_no_term(unsigned j) {
return
j >= lra.column_count()
||
!lra.column_has_term(j)
||
(ignore_big_nums() && term_has_big_number(lra.get_term(j)));
}
// Processes columns that have changed due to variables becoming fixed/unfixed or terms being updated.
// It identifies affected terms and rows, recalculates entries, removes irrelevant fresh definitions,
// and ensures substituted variables are properly eliminated from changed F entries, m_e_matrix.
// The function maintains internal consistency of data structures after these updates.
void process_m_changed_f_columns(std_vector<unsigned> &f_vector) {
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 >= lra.column_count() || if (!is_big_term_or_no_term(j))
!lra.column_has_term(j) ||
(ignore_big_nums() && term_has_big_number(lra.get_term(j)))
)
continue;
m_terms_to_tighten.insert(j); m_terms_to_tighten.insert(j);
if (j < m_l_matrix.column_count()) { if (j < m_l_matrix.column_count())
for (const auto& cs : m_l_matrix.column(j)) { for (const auto& cs : m_l_matrix.column(j))
m_changed_rows.insert(cs.var()); m_changed_rows.insert(cs.var());
} }
}
}
// find more entries to recalculate // find more entries to recalculate
std_vector<unsigned> more_changed_rows; std_vector<unsigned> more_changed_rows;
@ -1085,39 +1085,34 @@ namespace lp {
if (it == m_row2fresh_defs.end()) continue; if (it == m_row2fresh_defs.end()) continue;
for (unsigned xt : it->second) { for (unsigned xt : it->second) {
SASSERT(var_is_fresh(xt)); SASSERT(var_is_fresh(xt));
for (const auto& p : m_e_matrix.m_columns[xt]) { for (const auto& p : m_e_matrix.m_columns[xt])
more_changed_rows.push_back(p.var()); more_changed_rows.push_back(p.var());
} }
} }
}
for (unsigned ei : more_changed_rows) { for (unsigned ei : more_changed_rows)
m_changed_rows.insert(ei); m_changed_rows.insert(ei);
}
for (unsigned ei : m_changed_rows) { for (unsigned ei : m_changed_rows) {
if (ei >= m_e_matrix.row_count()) if (ei >= m_e_matrix.row_count())
continue; continue;
if (belongs_to_s(ei)) if (belongs_to_s(ei))
f_vector.push_back(ei); f_vector.push_back(ei);
recalculate_entry(ei); recalculate_entry(ei);
if (m_e_matrix.m_columns.back().size() == 0) { if (m_e_matrix.m_columns.back().size() == 0) {
m_e_matrix.m_columns.pop_back(); m_e_matrix.m_columns.pop_back();
m_var_register.shrink(m_e_matrix.column_count()); m_var_register.shrink(m_e_matrix.column_count());
} }
if (m_l_matrix.m_columns.back().size() == 0) { if (m_l_matrix.m_columns.back().size() == 0)
m_l_matrix.m_columns.pop_back(); m_l_matrix.m_columns.pop_back();
} }
}
remove_irrelevant_fresh_defs(); remove_irrelevant_fresh_defs();
eliminate_substituted_in_changed_rows(); eliminate_substituted_in_changed_rows();
m_changed_f_columns.reset(); m_changed_f_columns.reset();
m_changed_rows.reset(); m_changed_rows.reset();
m_changed_terms.reset(); m_changed_terms.reset();
SASSERT(entries_are_ok());
} }
int get_sign_in_e_row(unsigned ei, unsigned j) const { int get_sign_in_e_row(unsigned ei, unsigned j) const {
@ -1185,7 +1180,7 @@ namespace lp {
m_lra_level = 0; m_lra_level = 0;
reset_conflict(); reset_conflict();
process_changed_columns(f_vector); process_m_changed_f_columns(f_vector);
for (const lar_term* t : m_added_terms) { for (const lar_term* t : m_added_terms) {
m_active_terms.insert(t); m_active_terms.insert(t);
f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry
@ -1543,7 +1538,7 @@ namespace lp {
// print_bounds(tout); // print_bounds(tout);
); );
for (unsigned j : sorted_changed_terms) { for (unsigned j : sorted_changed_terms) {
if (ignore_big_nums() && term_has_big_number(lra.get_term(j))) { if (is_big_term_or_no_term(j)) {
m_terms_to_tighten.remove(j); m_terms_to_tighten.remove(j);
continue; continue;
} }
@ -1578,24 +1573,30 @@ namespace lp {
m_c = mpq(0); m_c = mpq(0);
m_lspace.clear(); m_lspace.clear();
m_lspace.add(mpq(1), lar_t.j()); m_lspace.add(mpq(1), lar_t.j());
bool ret = true;
SASSERT(get_extended_term_value(lar_t).is_zero()); SASSERT(get_extended_term_value(lar_t).is_zero());
for (const auto& p : lar_t) { for (const auto& p : lar_t) {
if (is_fixed(p.j())) { if (is_fixed(p.j())) {
const mpq& b = lia.lower_bound(p.j()).x; const mpq& b = lia.lower_bound(p.j()).x;
if (ignore_big_nums() && b.is_big()) if (ignore_big_nums() && b.is_big()) {
return false; ret = false;
break;
}
m_c += p.coeff() * b; m_c += p.coeff() * b;
} }
else { else {
unsigned lj = lar_solver_to_local(p.j()); unsigned lj = lar_solver_to_local(p.j());
SASSERT(!p.coeff().is_big()); if (ignore_big_nums() && p.coeff().is_big()) {
ret = false;
break;
}
m_espace.add(p.coeff(), lj);; m_espace.add(p.coeff(), lj);;
if (can_substitute(lj)) if (can_substitute(lj))
q.push(lj); q.push(lj);
} }
} }
SASSERT(subs_invariant(lar_t.j())); SASSERT(subs_invariant(lar_t.j()));
return true; return ret;
} }
unsigned lar_solver_to_local(unsigned j) const { unsigned lar_solver_to_local(unsigned j) const {
@ -2239,8 +2240,6 @@ namespace lp {
for (unsigned k = 0; k < lra.terms().size(); k++) { for (unsigned k = 0; k < lra.terms().size(); k++) {
const lar_term* t = lra.terms()[k]; const lar_term* t = lra.terms()[k];
if (!lia.column_is_int(t->j())) continue; if (!lia.column_is_int(t->j())) continue;
if (ignore_big_nums() && term_has_big_number(*t))
continue;
SASSERT(t->j() != UINT_MAX); SASSERT(t->j() != UINT_MAX);
for (const auto& p : (*t).ext_coeffs()) { for (const auto& p : (*t).ext_coeffs()) {
unsigned j = p.var(); unsigned j = p.var();
@ -2288,11 +2287,12 @@ namespace lp {
bool is_in_sync() const { bool is_in_sync() const {
for (unsigned j = 0; j < m_e_matrix.column_count(); j++) { for (unsigned j = 0; j < m_e_matrix.column_count(); j++) {
unsigned external_j = m_var_register.local_to_external(j); unsigned external_j = m_var_register.local_to_external(j);
if (external_j == UINT_MAX) continue; if (external_j == UINT_MAX)
if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) { continue;
// It is OK to have an empty column in m_e_matrix. if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size())
return false; return false;
} // It is OK to have an empty column in m_e_matrix.
} }
for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) { for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) {