3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 10:41:35 +00:00

cheap_eqs tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-15 16:08:53 -07:00
parent 274323b818
commit f7f9c15676
3 changed files with 28 additions and 20 deletions

View file

@ -61,7 +61,6 @@ public :
B & bp) { B & bp) {
bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp); bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
a.analyze(); a.analyze();
a.analyze_eq();
} }
private: private:
@ -328,21 +327,6 @@ private:
break; break;
} }
} }
void analyze_eq() {
switch (m_bp.lp().settings().cheap_eqs()) {
case 0:
return;
case 1:
m_bp.cheap_eq_tree(m_row_index);
break;
case 2:
m_bp.cheap_eq_table(m_row_index);
break;
default:
return;
}
}
}; };
} }

View file

@ -342,8 +342,28 @@ public:
if (settings().get_cancel_flag()) if (settings().get_cancel_flag())
return; return;
} }
// these two loops should be run sequentially
// since the first loop might change column bounds
// and add fixed columns this way
bp.clear_for_eq();
if (settings().cheap_eqs()) {
for (unsigned i : m_rows_with_changed_bounds) {
calculate_cheap_eqs_for_row(i, bp);
if (settings().get_cancel_flag())
return;
}
}
m_rows_with_changed_bounds.clear(); m_rows_with_changed_bounds.clear();
} }
template <typename T>
void calculate_cheap_eqs_for_row(unsigned i, lp_bound_propagator<T> & bp) {
if (settings().cheap_eqs() == 1) {
bp.cheap_eq_tree(i);
} else {
bp.cheap_eq_table(i);
}
}
bool is_fixed(column_index const& j) const { return column_is_fixed(j); } bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
bool external_is_used(unsigned) const; bool external_is_used(unsigned) const;

View file

@ -501,8 +501,10 @@ public:
clear_for_eq(); clear_for_eq();
unsigned x_index, y_index; unsigned x_index, y_index;
mpq offset; mpq offset;
if (!is_offset_row_wrong(row_index, x_index, y_index, offset)) if (!is_offset_row_wrong(row_index, x_index, y_index, offset)) {
m_visited_rows.insert(row_index);
return; return;
}
TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index);); TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
m_root = alloc(vertex, row_index, x_index, mpq(0)); m_root = alloc(vertex, row_index, x_index, mpq(0));
vertex* v_y = alloc(vertex, row_index, y_index, offset); vertex* v_y = alloc(vertex, row_index, y_index, offset);
@ -541,11 +543,13 @@ public:
unsigned row_index = c.var(); unsigned row_index = c.var();
if (m_visited_rows.contains(row_index)) if (m_visited_rows.contains(row_index))
continue; continue;
m_visited_rows.insert(row_index);
unsigned x_index, y_index; unsigned x_index, y_index;
mpq row_offset; mpq row_offset;
if (!is_offset_row_wrong(row_index, x_index, y_index, row_offset)) if (!is_offset_row_wrong(row_index, x_index, y_index, row_offset)) {
m_visited_rows.insert(row_index);
continue; continue;
}
m_visited_rows.insert(row_index);
TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index);); TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
// who is it the same column? // who is it the same column?
if (lp().get_row(row_index)[x_index].var() == j) { // conected to x if (lp().get_row(row_index)[x_index].var() == j) { // conected to x