From 1e4e887221d67f780d21efc044ad29e0d382ab01 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Jun 2020 12:38:31 -0700 Subject: [PATCH] propagate cheap eqs Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 62 +++++++++++------------------ src/math/lp/indexed_vector.h | 2 +- src/math/lp/lar_solver.h | 46 +++------------------ src/math/lp/lp_bound_propagator.h | 49 ++++++++++++++++++++++- src/smt/theory_lra.cpp | 1 - 5 files changed, 78 insertions(+), 82 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 353859e63..96f1260c4 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -13,9 +13,8 @@ Abstract: In the same loop trying to pin variables by pushing the partial sum up, denoting the variable related to it by _l Author: - - Lev Nachmanson (levnach) - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) Revision History: @@ -31,7 +30,7 @@ template // C plays a role of a container, B - lp_bound class bound_analyzer_on_row { const C& m_row; B & m_bp; - unsigned m_row_or_term_index; + unsigned m_row_index; int m_column_of_u; // index of an unlimited from above monoid // -1 means that such a value is not found, -2 means that at least two of such monoids were found int m_column_of_l; // index of an unlimited from below monoid @@ -48,7 +47,7 @@ public : : m_row(it), m_bp(bp), - m_row_or_term_index(row_or_term_index), + m_row_index(row_or_term_index), m_column_of_u(-1), m_column_of_l(-1), m_rs(rs) @@ -62,7 +61,7 @@ public : B & bp) { bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp); a.analyze(); - // TBD: a.analyze_eq(); + a.analyze_eq(); } private: @@ -84,37 +83,6 @@ private: limit_all_monoids_from_above(); } - - void analyze_eq() { - lpvar x = null_lpvar, y = null_lpvar; - for (const auto & c : m_row) { - if (m_bp.get_column_type(c.var()) == column_type::fixed) - continue; - if (x == null_lpvar && c.coeff().is_one()) - x = c.var(); - else if (y == null_lpvar && c.coeff().is_minus_one()) - y = c.var(); - else - return; - } - if (x == null_lpvar || y == null_lpvar) - return; - impq value; - for (const auto & c : m_row) { - if (m_bp.get_column_type(c.var()) == column_type::fixed) - value += c.coeff() * lb(c.var()); - } - if (!value.is_zero()) { - // insert / check offset table to infer equalities - // of the form y = z from offset table collision: - // value = (x - y) - // value = (x - z) - } - else { - // m_bp.try_add_fixed(x, y, m_row_or_term_index); - } - } - bool bound_is_available(unsigned j, bool lower_bound) { return (lower_bound && lower_bound_is_available(j)) || (!lower_bound && upper_bound_is_available(j)); @@ -327,7 +295,7 @@ private: // } void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ - m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_or_term_index, strict); + m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_index, strict); } void advance_u(unsigned j) { @@ -361,6 +329,24 @@ private: } } + void analyze_eq() { + unsigned x = UINT_MAX, y = UINT_MAX; + unsigned k = 0; + for (const auto& c : m_row) { + if (!m_bp.lp().column_is_fixed(c.var())) { + if (x == UINT_MAX && c.coeff().is_one()) + x = k; + else if (y == UINT_MAX && c.coeff().is_minus_one()) + y = k; + else + return; + } + k++; + } + if (x == UINT_MAX || y == UINT_MAX) + return; + m_bp.try_create_eq(x, y, m_row_index); + } }; } diff --git a/src/math/lp/indexed_vector.h b/src/math/lp/indexed_vector.h index 22d51e190..017a25f6b 100644 --- a/src/math/lp/indexed_vector.h +++ b/src/math/lp/indexed_vector.h @@ -83,7 +83,7 @@ public: return m_data.size(); } - unsigned size() { + unsigned size() const { return m_index.size(); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 82285a5e6..7555ea388 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -161,20 +161,7 @@ class lar_solver : public column_namer { bool use_lu() const; bool sizes_are_correct() const; bool implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const; - template - void analyze_new_bounds_on_row( - unsigned row_index, - lp_bound_propagator& bp) { - lp_assert(!use_tableau()); - unsigned j = m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row - bound_analyzer_on_row, lp_bound_propagator>::analyze_row( - m_mpq_lar_core_solver.get_pivot_row(), - j, - zero_of_type>(), - row_index, - bp); - } - + template void analyze_new_bounds_on_row_tableau( unsigned row_index, @@ -196,17 +183,8 @@ class lar_solver : public column_namer { void substitute_basis_var_in_terms_for_row(unsigned i); template void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) { - if (use_tableau()) { - analyze_new_bounds_on_row_tableau(i, bp); - } else { - m_mpq_lar_core_solver.calculate_pivot_row(i); - substitute_basis_var_in_terms_for_row(i); - analyze_new_bounds_on_row(i, bp); - } - } - template - void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) { - NOT_IMPLEMENTED_YET(); + SASSERT(use_tableau()); + analyze_new_bounds_on_row_tableau(i, bp); } static void clean_popped_elements(unsigned n, u_set& set); static void shrink_inf_set_after_pop(unsigned n, u_set & set); @@ -346,28 +324,14 @@ public: void activate(constraint_index ci); void random_update(unsigned sz, var_index const * vars); template - void propagate_bounds_on_terms(lp_bound_propagator & bp) { - for (unsigned i = 0; i < m_terms.size(); i++) { - if (term_is_used_as_row(i)) - continue; // this term is used a left side of a constraint, - // it was processed as a touched row if needed - propagate_bounds_on_a_term(*m_terms[i], bp, i); - } - } - template void propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { - if (!use_tableau()) - return; // todo: consider to remove the restriction - + SASSERT(use_tableau()); for (unsigned i : m_rows_with_changed_bounds) { calculate_implied_bounds_for_row(i, bp); if (settings().get_cancel_flag()) return; } m_rows_with_changed_bounds.clear(); - if (!use_tableau()) { - propagate_bounds_on_terms(bp); - } } 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)); } @@ -591,7 +555,7 @@ public: return false; } void round_to_integer_solution(); - inline const row_strip & get_row(unsigned i) { return A_r().m_rows[i]; } + inline const row_strip & get_row(unsigned i) const { return A_r().m_rows[i]; } bool row_is_correct(unsigned i) const; bool ax_is_correct() const; bool get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq &rs, constraint_index& ci, bool &upper_bound) const; diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9049b17b2..316fb0914 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -1,18 +1,40 @@ /* Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson + Author: + Nickolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) */ #pragma once #include "math/lp/lp_settings.h" namespace lp { template class lp_bound_propagator { + + // defining a graph on columns x, y such that there is a row x - y = c, where c is a constant + struct vertex { + unsigned m_row; + unsigned m_index; // in the row + bool m_sign; // true if the vertex plays the role of y + vector m_adjacent_edges; // points to the + vertex(unsigned row, unsigned index) : m_row(row), m_index(index) {} + }; + + // an edge can be between columns in the same row or between two different rows in the same column + struct edge { + unsigned m_a; + unsigned m_b; + impq m_offset; + }; + vector m_vertices; + vector m_edges; + std::unordered_map m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_upper_bounds; T& m_imp; public: vector m_ibounds; lp_bound_propagator(T& imp): m_imp(imp) {} + const lar_solver& lp() const { return m_imp.lp(); } column_type get_column_type(unsigned j) const { return m_imp.lp().get_column_type(j); } @@ -65,5 +87,30 @@ public: void consume(const mpq& a, constraint_index ci) { m_imp.consume(a, ci); } + + void create_initial_xy(unsigned x, unsigned y, unsigned row_index) { + impq value; + const auto& row = lp().get_row(row_index); + for (unsigned k = 0; k < row.size(); k++) { + if (k == x || k == y) + continue; + const auto& c = row[k]; + value += c.coeff() * lp().get_lower_bound(c.var()); + } + vertex xv(row_index, x); + m_vertices.push_back(xv); + vertex yv(row_index, y); + m_vertices.push_back(yv); + + NOT_IMPLEMENTED_YET(); + } + + void try_create_eq(unsigned x, unsigned y, unsigned row_index) { + m_vertices.clear(); + m_edges.clear(); + create_initial_xy(x, y, row_index); + NOT_IMPLEMENTED_YET(); + + } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a545d7215..386441c51 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -4033,4 +4033,3 @@ template class lp::lp_bound_propagator; template void lp::lar_solver::propagate_bounds_for_touched_rows(lp::lp_bound_propagator&); template void lp::lar_solver::explain_implied_bound(lp::implied_bound&, lp::lp_bound_propagator&); template void lp::lar_solver::calculate_implied_bounds_for_row(unsigned int, lp::lp_bound_propagator&); -template void lp::lar_solver::propagate_bounds_on_terms(lp::lp_bound_propagator&);