From 29b3f438bcf82c3e8c3a622dee01ca6e5821fde5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 1 Jul 2020 19:02:30 -0700 Subject: [PATCH] cheap_eqs - work on fixed_phase Signed-off-by: Lev Nachmanson --- src/math/lp/lp_bound_propagator.h | 279 +++++++++++++++++------------- 1 file changed, 161 insertions(+), 118 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 511e5f059..f483f9275 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -25,24 +25,19 @@ class lp_bound_propagator { vertex* m_parent; unsigned m_level; // the distance in hops to the root; // it is handy to find the common ancestor - bool m_neg; // false if grows with the root, true if grows with -root public: vertex() {} vertex(unsigned row, - unsigned column, - bool neg) : + unsigned column) : m_row(row), m_column(column), m_parent(nullptr), - m_level(0), - m_neg(neg) + m_level(0) {} unsigned column() const { return m_column; } unsigned row() const { return m_row; } vertex* parent() const { return m_parent; } unsigned level() const { return m_level; } - bool neg() const { return m_neg; } - bool& neg() { return m_neg; } void add_child(vertex* child) { SASSERT(!(*this == *child)); child->m_parent = this; @@ -50,17 +45,24 @@ class lp_bound_propagator { child->m_level = m_level + 1; } const ptr_vector & children() const { return m_children; } - std::ostream& print(std::ostream & out) const { - out << "r = " << m_row << ", c = " << m_column << ", P = {"; - if (m_parent) { out << "(" << m_parent->row() << ", " << m_parent->column() << ")";} - else { out << "null"; } - out << "} , lvl = " << m_level << (neg()? " -":" +"); - return out; - } bool operator==(const vertex& o) const { return m_row == o.m_row && m_column == o.m_column; } }; + + std::ostream& print(std::ostream & out, const vertex* v) const { + out << "r = " << v->row() << ", c = " << v->column() << ", P = {"; + if (v->parent()) { out << "(" << v->parent()->row() << ", " << v->parent()->column() << ")";} + else { out << "null"; } + out << "} , lvl = " << v->level(); + if (m_pol.contains(v->column())) { + tout << (pol(v) == -1? " -":" +"); + } else { + tout << " not in m_pol"; + } + return out; + } + hashtable m_visited_rows; hashtable m_visited_columns; vertex* m_root; @@ -69,26 +71,20 @@ class lp_bound_propagator { // by adjusting the vertices offsets, so they become absolute. // If the tree is fixed then in addition to checking with the m_vals_to_verts // we are going to check with the m_fixed_var_tables. - vertex* m_fixed_vertex; + const vertex* m_fixed_vertex; + explanation m_fixed_vertex_explanation; // a pair (o, j) belongs to m_vals_to_verts iff x[j] = x[m_root->column()] + o map, default_eq> m_vals_to_verts; // a pair (o, j) belongs to m_vals_to_verts_neg iff -x[j] = x[m_root->column()] + o map, default_eq> m_vals_to_verts_neg; + // x[m_root->column()] - m_pol[j]*x[j] == const; + u_map m_pol; + // if m_pos.contains(j) then x[j] = x[m_root->column()] + o + uint_set m_pos; + // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_lower_bounds; std::unordered_map m_improved_upper_bounds; - class signed_column { - bool m_sign; - unsigned m_column; - public: - signed_column() : m_column(UINT_MAX) {} - bool not_set() const { return m_column == UINT_MAX; } - bool is_set() const { return m_column != UINT_MAX; } - bool sign() const { return m_sign; } - bool& sign() { return m_sign; } - unsigned column() const { return m_column; } - unsigned& column() { return m_column; } - }; T& m_imp; vector m_ibounds; @@ -172,19 +168,6 @@ public: m_imp.consume(a, ci); } - bool set_sign_and_column(signed_column& i, const row_cell & c) const { - if (c.coeff().is_one()) { - i.sign() = false; - i.column() = c.var(); - return true; - } - else if (c.coeff().is_minus_one()){ - i.sign() = true; - i.column() = c.var(); - return true; - } - return false; - } const mpq& val(unsigned j) const { return lp().get_column_value(j).x; } @@ -200,11 +183,11 @@ public: if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) return; TRACE("cheap_eq", tout << "found j=" << j << " for v="; - v->print(tout) << "\n in lp.fixed tables\n";); - ptr_vector path; + print(tout, v) << "\n in lp.fixed tables\n";); + ptr_vector path; find_path_on_tree(path, v, m_fixed_vertex); explanation ex = get_explanation_from_path(path); - explain_fixed_column(ex, j); + ex.add_expl(m_fixed_vertex_explanation); add_eq_on_columns(ex, j, v->column()); } @@ -217,6 +200,47 @@ public: } return false; } + + // pol for polarity + int pol(const vertex* v) const { return pol(v->column()); } + int pol(unsigned j) const { return m_pol[j]; } + void set_polarity(unsigned j, int p) { + SASSERT(p == 1 || p == -1); + SASSERT(!m_pol.contains(j)); + m_pol.insert(j, p); + } + + void check_polarity(vertex* v, int polarity) { + int prev_pol; + if (!m_pol.find(v->column(), prev_pol)) { + m_pol.insert(v->column(), polarity); + return; + } + if (prev_pol == polarity) + return; + TRACE("cheap_eq", tout << "polarity switch:"; print(tout , v) << "\n";); + const vertex *u = find_other_vertex_with_same_column(v); + ptr_vector path; + find_path_on_tree(path, u, v); + m_fixed_vertex_explanation = get_explanation_from_path(path); + set_fixed_vertex(v); + } + + const vertex* find_other_vertex_with_same_column(const vertex* t) const { + return find_other_vertex_with_same_column_under(m_root, t); + } + + const vertex * find_other_vertex_with_same_column_under(const vertex* v, const vertex* t) const { + if (v != t && v->column() == t->column()) + return v; + for (const vertex* c : v->children()) { + auto u = find_other_vertex_with_same_column_under(c, t); + if (u) + return u; + } + UNREACHABLE(); + return nullptr; + } bool tree_contains(vertex *v) const { if (!m_root) @@ -224,28 +248,34 @@ public: return tree_contains_r(m_root, v); } - vertex * alloc_v(unsigned row_index, unsigned column, bool neg) { - vertex * v = alloc(vertex, row_index, column, neg); + vertex * alloc_v(unsigned row_index, unsigned column) { + vertex * v = alloc(vertex, row_index, column); SASSERT(!tree_contains(v)); return v; } + + static bool not_set(unsigned j) { return j == UINT_MAX; } + static bool is_set(unsigned j) { return j != UINT_MAX; } void create_root(unsigned row_index) { SASSERT(!m_root && !m_fixed_vertex); - signed_column x, y; + unsigned x, y; + int polarity; TRACE("cheap_eq", print_row(tout, row_index);); - if (!is_tree_offset_row(row_index, x, y)) { + if (!is_tree_offset_row(row_index, x, y, polarity)) { TRACE("cheap_eq", tout << "not an offset row\n";); return; } - const mpq& r = val(x.column()); - m_root = alloc_v(row_index, x.column(), false); - if (y.not_set()) { - set_fixed_vertex(m_root); + const mpq& r = val(x); + m_root = alloc_v(row_index, x); + set_polarity(x, 1); + if (not_set(y)) { + set_fixed_vertex(m_root); + explain_fixed_in_row(row_index, m_fixed_vertex_explanation); } else { - bool neg = x.sign() == y.sign(); - vertex *v = alloc_v(row_index, y.column(), neg); + vertex *v = alloc_v(row_index, y); m_root->add_child(v); + set_polarity(y, polarity); } // keep root in the positive table m_vals_to_verts.insert(r, m_root); @@ -261,29 +291,33 @@ public: // It is assumed that parent->column() is present in the row vertex* add_child_from_row(unsigned row_index, vertex* parent) { TRACE("cheap_eq", print_row(tout, row_index);); - signed_column x, y; - if (!is_tree_offset_row(row_index, x, y)) { + unsigned x, y; int polarity; + if (!is_tree_offset_row(row_index, x, y, polarity)) { TRACE("cheap_eq", tout << "not an offset row\n"; ); return nullptr; } - if (y.not_set()) { - SASSERT(parent->column() == x.column()); - vertex *v = alloc_v( row_index, x.column(), parent->neg()); + if (not_set(y)) { + SASSERT(parent->column() == x); + vertex *v = alloc_v(row_index, x); parent->add_child(v); - set_fixed_vertex(v); + if (!fixed_phase()) { + set_fixed_vertex(v); + explain_fixed_in_row(row_index, m_fixed_vertex_explanation); + } return v; } - SASSERT(x.is_set() && y.is_set()); + SASSERT(is_set(x) && is_set(y)); - // v is exactly like parent, but the row is different - vertex *v = alloc_v(row_index, parent->column(), parent->neg()); + // v has the column of the parent, but the row is different + vertex *v = alloc_v(row_index, parent->column()); parent->add_child(v); - SASSERT(x.column() == v->column() || y.column() == v->column()); - unsigned col = v->column() == y.column()? x.column(): y.column(); - bool neg = x.sign() == y.sign() ? !v->neg(): v->neg(); - vertex *vy = alloc_v(v->row(), col, neg); + SASSERT(x == v->column() || y == v->column()); + unsigned col = v->column() == y? x : y; + vertex *vy = alloc_v(v->row(), col); v->add_child(vy); + if (!fixed_phase()) + check_polarity(vy, polarity * pol(v)); return v; } @@ -292,25 +326,31 @@ public: } void check_for_eq_and_add_to_val_table(vertex* v, map, default_eq>& table) { + TRACE("cheap_eq", tout << "v="; print(tout, v) << "\n";); vertex *k; // the other vertex if (table.find(val(v), k)) { - TRACE("cheap_eq", tout << "found k " ; k->print(tout) << "\n";); + TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";); if (k->column() != v->column() && is_int(k->column()) == is_int(v->column()) && - !is_equal(k->column(), v->column())) + !is_equal(k->column(), v->column())) { report_eq(k, v); + } else { + TRACE("cheap_eq", tout << "no report\n";); + } } else { - TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; v->print(tout) << "} \n";); + TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print(tout, v) << "} \n";); table.insert(val(v), v); } } void check_for_eq_and_add_to_val_tables(vertex* v) { - TRACE("cheap_eq_det", v->print(tout) << "\n";); - if (v->neg()) - check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg); - else - check_for_eq_and_add_to_val_table(v, m_vals_to_verts); + TRACE("cheap_eq_det", print(tout, v) << "\n";); + if (!fixed_phase()) { + if (pol(v->column()) == -1) + check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg); + else + check_for_eq_and_add_to_val_table(v, m_vals_to_verts); + } } void clear_for_eq() { @@ -319,11 +359,11 @@ public: m_root = nullptr; } - std::ostream& print_path(const ptr_vector& path, std::ostream& out) const { + std::ostream& print_path(const ptr_vector& path, std::ostream& out) const { unsigned pr = UINT_MAX; out << "path = \n"; - for (vertex* k : path) { - k->print(out) << "\n"; + for (const vertex* k : path) { + print(out, k) << "\n"; if (k->row() != pr) { print_row(out, pr = k->row()); } @@ -336,13 +376,13 @@ public: SASSERT(v_i != v_j); SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column())); TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = "; - v_i->print(tout) << "\nv = "; v_j->print(tout) <<"\n"; + print(tout, v_i) << "\nv = "; print(tout, v_j) <<"\n"; display_row_of_vertex(v_i, tout); if (v_j->row() != v_i->row()) display_row_of_vertex(v_j, tout); ); - ptr_vector path; + ptr_vector path; find_path_on_tree(path, v_i, v_j); lp::explanation exp = get_explanation_from_path(path); add_eq_on_columns(exp, v_i->column(), v_j->column()); @@ -364,19 +404,6 @@ public: lp().settings().stats().m_cheap_eqs++; } - /** - The table functionality: - Cheap propagation of equalities x_i = x_j, when - x_i = y + k - x_j = y + k - - This equalities are detected by maintaining a map: - (y, k) -> row_id when a row is of the form x = y + k - If x = k, then y is null_lpvar - This methods checks whether the given row is an offset row (is_offset_row()) - and uses the map to find new equalities if that is the case. - Some equalities, those spreading more than two rows, can be missed - */ // column to theory_var unsigned col_to_imp(unsigned j) const { return lp().local_to_external(lp().column_to_reported_index(j)); @@ -391,10 +418,10 @@ public: return lp().column_is_int(j); } - explanation get_explanation_from_path(const ptr_vector& path) const { + explanation get_explanation_from_path(const ptr_vector& path) const { explanation ex; unsigned prev_row = UINT_MAX; - for (vertex* k : path) { + for (const vertex* k : path) { unsigned row = k->row(); if (row == prev_row) continue; @@ -423,11 +450,11 @@ public: return print_row(out, k->row()); } - void find_path_on_tree(ptr_vector & path, vertex* u, vertex* v) const { - TRACE("cheap_eq_details", tout << "u = " ;u->print(tout); tout << "\nv = ";v->print(tout) << "\n";); + void find_path_on_tree(ptr_vector & path, const vertex* u, const vertex* v) const { + TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = ";print(tout, v) << "\n";); vertex* up; // u parent vertex* vp; // v parent - ptr_vector v_branch; + vector v_branch; path.push_back(u); v_branch.push_back(v); // equalize the levels @@ -445,7 +472,7 @@ public: v = vp; } SASSERT(u->level() == v->level()); - TRACE("cheap_eq_details", tout << "u = " ;u->print(tout); tout << "\nv = ";v->print(tout) << "\n";); + TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = "; print(tout, v) << "\n";); while (u != v) { up = u->parent(); vp = v->parent(); @@ -457,7 +484,7 @@ public: } for (unsigned i = v_branch.size(); i--; ) { - vertex * bv = v_branch[i]; + const vertex * bv = v_branch[i]; if (path.back() != bv) path.push_back(bv); } @@ -477,8 +504,8 @@ public: return false; } bool tree_is_correct(vertex* v, ptr_vector& vs) const { - if (fixed_phase() && v->neg()) - return false; + if (fixed_phase()) + return true; for (vertex * u : v->children()) { if (contains_vertex(u, vs)) return false; @@ -495,7 +522,7 @@ public: return true; } std::ostream& print_tree(std::ostream & out, vertex* v) const { - v->print(out); + print(out, v); out << "\nchildren :\n"; for (auto * c : v->children()) { print_tree(out, c); @@ -514,16 +541,15 @@ public: TRACE("cheap_eq", tout << "tree = "; print_tree(tout, m_root) << "\n";); SASSERT(tree_is_correct()); explore_under(m_root); - if (fixed_phase()) { - create_fixed_eqs(m_root); - } TRACE("cheap_eq", tout << "done for row_index " << row_index << "\n";); TRACE("cheap_eq", tout << "tree size = " << verts_size();); delete_tree(m_root); m_root = nullptr; set_fixed_vertex(nullptr); + m_fixed_vertex_explanation.clear(); m_vals_to_verts.reset(); m_vals_to_verts_neg.reset(); + m_pol.reset(); } void create_fixed_eqs(vertex* v) { @@ -533,8 +559,8 @@ public: } std::ostream& print_row(std::ostream & out, unsigned row_index) const { - signed_column x, y; - if (true || !is_tree_offset_row(row_index, x, y)) + unsigned x, y; int polarity; + if (true || !is_tree_offset_row(row_index, x, y, polarity)) return lp().get_int_solver()->display_row_info(out, row_index); bool first = true; @@ -553,12 +579,13 @@ public: out << "\n"; return out; } - - void set_fixed_vertex(vertex *v) { - TRACE("cheap_eq", if (v) v->print(tout); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";); + void set_fixed_vertex(vertex *v) { + TRACE("cheap_eq", if (v) print(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";); + SASSERT(!m_fixed_vertex || v == nullptr); m_fixed_vertex = v; } + unsigned verts_size() const { return subtree_size(m_root); } @@ -612,23 +639,39 @@ public: // In case of only one non fixed column, and the function returns true, // this column would be represened by x. bool is_tree_offset_row( unsigned row_index, - signed_column & x, - signed_column & y) const { + unsigned & x, unsigned & y, int & polarity ) const { + x = y = UINT_MAX; + const row_cell* x_cell = nullptr; + const row_cell* y_cell = nullptr; const auto & row = lp().get_row(row_index); for (unsigned k = 0; k < row.size(); k++) { const auto& c = row[k]; if (column_is_fixed(c.var())) continue; - if (x.not_set()) { - if (!set_sign_and_column(x, c)) + if (not_set(x)) { + if (c.coeff().is_one() || c.coeff().is_minus_one()) { + x = c.var(); + x_cell = & c; + } else { return false; - } else if (y.not_set()) { - if (!set_sign_and_column(y, c)) + } + } else if (not_set(y)) { + if (c.coeff().is_one() || c.coeff().is_minus_one()) { + y = c.var(); + y_cell = & c; + } else return false; } else return false; } - return x.is_set() || y.is_set(); - } + if (is_set(x)) { + if (is_set(y)) + polarity = x_cell->coeff().is_pos() == y_cell->coeff().is_pos()? -1 : 1; + else + polarity = 1; + return true; + } + return false; + } }; }