mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 03:15:41 +00:00
Code Activity

debug tighten_bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-04 10:46:07 -10:00
parent 1612eafaeb
commit f4f199faf7
2 changed files with 36 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -480,7 +480,7 @@ namespace lp {
std::unordered_map<unsigned, std_vector<unsigned>> m_row2fresh_defs; std::unordered_map<unsigned, std_vector<unsigned>> m_row2fresh_defs;
indexed_uint_set m_changed_rows; indexed_uint_set m_changed_rows;
indexed_uint_set m_changed_columns; indexed_uint_set m_new_fixed_columns;
indexed_uint_set m_changed_terms; // a term is defined by its column j, as in lar_solver.get_term(j) indexed_uint_set m_changed_terms; // a term is defined by its column j, as in lar_solver.get_term(j)
indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase, indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase,
// m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
@ -718,7 +718,7 @@ namespace lp {
void add_changed_column(unsigned j) { void add_changed_column(unsigned j) {
TRACE("dioph_eq", lra.print_column_info(j, tout);); TRACE("dioph_eq", lra.print_column_info(j, tout););
m_changed_columns.insert(j); m_new_fixed_columns.insert(j);
} }
std_vector<const lar_term*> m_added_terms; std_vector<const lar_term*> m_added_terms;
std::unordered_set<const lar_term*> m_active_terms; std::unordered_set<const lar_term*> m_active_terms;
@ -748,7 +748,7 @@ namespace lp {
void update_column_bound_callback(unsigned j) { void update_column_bound_callback(unsigned j) {
if (!lra.column_is_int(j) || !lra.column_is_fixed(j)) if (!lra.column_is_int(j) || !lra.column_is_fixed(j))
return; return;
m_changed_columns.insert(j); m_new_fixed_columns.insert(j);
auto undo = undo_fixed_column(*this, j); auto undo = undo_fixed_column(*this, j);
lra.trail().push(undo); lra.trail().push(undo);
} }
@ -937,7 +937,7 @@ namespace lp {
} }
void find_changed_terms_and_more_changed_rows() { void find_changed_terms_and_more_changed_rows() {
for (unsigned j : m_changed_columns) { for (unsigned j : m_new_fixed_columns) {
const auto it = m_columns_to_terms.find(j); const auto it = m_columns_to_terms.find(j);
if (it != m_columns_to_terms.end()) if (it != m_columns_to_terms.end())
for (unsigned k : it->second) { for (unsigned k : it->second) {
@ -1027,8 +1027,8 @@ namespace lp {
remove_irrelevant_fresh_defs(); remove_irrelevant_fresh_defs();
eliminate_substituted_in_changed_rows(); eliminate_substituted_in_changed_rows();
m_changed_columns.reset(); m_new_fixed_columns.reset();
SASSERT(m_changed_columns.size() == 0); SASSERT(m_new_fixed_columns.size() == 0);
m_changed_rows.reset(); m_changed_rows.reset();
SASSERT(entries_are_ok()); SASSERT(entries_are_ok());
} }
@ -1478,7 +1478,7 @@ namespace lp {
lra.print_explanation(out, lra.flatten(b.m_dep)); lra.print_explanation(out, lra.flatten(b.m_dep));
return out; return out;
} }
// h is the entry that has been moved to S // h is the entry that is ready to be moved to S
lia_move tighten_bounds(unsigned h) { lia_move tighten_bounds(unsigned h) {
protected_queue q; protected_queue q;
copy_row_to_espace_in_lar_indices(h); copy_row_to_espace_in_lar_indices(h);
@ -2626,6 +2626,26 @@ namespace lp {
m_k2s.add(k, h); m_k2s.add(k, h);
} }
void update_entries_with_new_fixed(std_vector<unsigned> & f_vector) {
std::vector<unsigned> deb_upd;
for (unsigned j : m_new_fixed_columns) {
SASSERT(is_fixed(j));
j = lar_solver_to_local(j);
for (auto & c : m_e_matrix.m_columns[j]) {
unsigned ei = c.var();
m_sum_of_fixed[ei] += lra.get_lower_bound(j).x;
unsigned offset_in_row = c.offset();
m_e_matrix.remove_element(ei, m_e_matrix.m_rows[ei][offset_in_row]);
if (belongs_to_s(ei)) {
remove_from_S(ei);
f_vector.push_back(ei);
}
}
}
SASSERT(entries_are_ok());
}
// this is the step 6 or 7 of the algorithm // this is the step 6 or 7 of the algorithm
// returns true if an equlity was rewritten and false otherwise // returns true if an equlity was rewritten and false otherwise
bool rewrite_eqs(std_vector<unsigned>& f_vector) { bool rewrite_eqs(std_vector<unsigned>& f_vector) {
@ -2683,16 +2703,13 @@ namespace lp {
SASSERT(h == f_vector[ih]); SASSERT(h == f_vector[ih]);
if (min_ahk.is_one()) { if (min_ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout);); TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout););
SASSERT(m_changed_columns.size() == 0); SASSERT(m_new_fixed_columns.size() == 0);
if (tighten_bounds(h) == lia_move::conflict){ if (tighten_bounds(h) == lia_move::conflict){
if (m_changed_columns.size()) { // need to process this entry, and the entries containing the new fixed, again
std::cout << "m_changed_columns: " << m_changed_columns.size() << "\n";
NOT_IMPLEMENTED_YET();
}
return false; return false;
} }
if (m_changed_columns.size()) { // need to process this entry, and the entries containing the new fixed, again if (m_new_fixed_columns.size()) { // Need to update all entries containing the new fixed columns.
NOT_IMPLEMENTED_YET(); // The previous calculations in the loop might be invalid
update_entries_with_new_fixed(f_vector);
return true; return true;
} }
move_entry_from_f_to_s(kh, h); move_entry_from_f_to_s(kh, h);

5
src/math/lp/static_matrix.h
View file

@ -145,6 +145,11 @@ public:
void add_columns_up_to(unsigned j) { while (j >= column_count()) add_column(); } void add_columns_up_to(unsigned j) { while (j >= column_count()) add_column(); }
void remove_element(std_vector<row_cell<T>> & row, row_cell<T> & elem_to_remove); void remove_element(std_vector<row_cell<T>> & row, row_cell<T> & elem_to_remove);
void remove_element(unsigned ei, row_cell<T> & elem_to_remove) {
remove_element(m_rows[ei], elem_to_remove);
}
void multiply_column(unsigned column, T const & alpha) { void multiply_column(unsigned column, T const & alpha) {
for (auto & t : m_columns[column]) { for (auto & t : m_columns[column]) {