From 742be835031e824c371f64d6392442150c923c65 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Jun 2020 01:00:06 -0700 Subject: [PATCH] Lpbounds (#4492) * remove inheritance from bound propagation Signed-off-by: Lev Nachmanson * less inheritance Signed-off-by: Lev Nachmanson * less inheritance Signed-off-by: Lev Nachmanson * fix the build Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/bound_analyzer_on_row.h | 10 +-- src/math/lp/lar_solver.cpp | 96 ---------------------------- src/math/lp/lar_solver.h | 97 ++++++++++++++++++++++++++--- src/math/lp/lp_bound_propagator.cpp | 54 ---------------- src/math/lp/lp_bound_propagator.h | 69 +++++++++++++++----- src/smt/theory_lra.cpp | 62 +++++++++--------- src/smt/theory_lra.h | 2 + src/test/lp/lp.cpp | 5 -- 9 files changed, 185 insertions(+), 211 deletions(-) delete mode 100644 src/math/lp/lp_bound_propagator.cpp diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 34892c7e0..f40ae6038 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(lp SOURCES binary_heap_priority_queue.cpp binary_heap_upair_queue.cpp - lp_bound_propagator.cpp core_solver_pretty_printer.cpp dense_matrix.cpp eta_matrix.cpp diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 409dda96d..353859e63 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -24,14 +24,13 @@ Revision History: #include "util/vector.h" #include "math/lp/implied_bound.h" -#include "math/lp/lp_bound_propagator.h" #include "math/lp/test_bound_analyzer.h" namespace lp { -template // C plays a role of a container +template // C plays a role of a container, B - lp_bound_propagator class bound_analyzer_on_row { const C& m_row; - lp_bound_propagator & m_bp; + B & m_bp; unsigned m_row_or_term_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 @@ -45,7 +44,7 @@ public : unsigned bj, // basis column for the row const numeric_pair& rs, unsigned row_or_term_index, - lp_bound_propagator & bp) + B & bp) : m_row(it), m_bp(bp), @@ -55,11 +54,12 @@ public : m_rs(rs) {} + static void analyze_row(const C & row, unsigned bj, // basis column for the row const numeric_pair& rs, unsigned row_or_term_index, - lp_bound_propagator & bp) { + B & bp) { bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp); a.analyze(); // TBD: a.analyze_eq(); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 83a8619e3..f479b4d33 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -135,23 +135,6 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, return kind == be.kind() && rs_of_evidence == be.m_bound; } - -void lar_solver::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>::analyze_row( - m_mpq_lar_core_solver.get_pivot_row(), - j, - zero_of_type>(), - row_index, - bp - ); -// ra_pos.analyze(); -} bool lar_solver::row_has_a_big_num(unsigned i) const { for (const auto& c : A_r().m_rows[i]) { @@ -161,23 +144,6 @@ bool lar_solver::row_has_a_big_num(unsigned i) const { return false; } -void lar_solver::analyze_new_bounds_on_row_tableau( - unsigned row_index, - lp_bound_propagator & bp ) { - - if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation - || row_has_a_big_num(row_index)) - return; - lp_assert(use_tableau()); - - bound_analyzer_on_row>::analyze_row(A_r().m_rows[row_index], - null_ci, - zero_of_type>(), - row_index, - bp - ); -} - void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { // todo : create a map from term basic vars to the rows where they are used @@ -190,16 +156,6 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); } } - -void lar_solver::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); - } -} unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { if (!tv::is_term(j)) { @@ -213,64 +169,12 @@ unsigned lar_solver::map_term_index_to_column_index(unsigned j) const { SASSERT(tv::is_term(j)); return m_var_register.external_to_local(j); } - -void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) { - lp_assert(false); // not implemented -} - - -void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) { - unsigned i = ib.m_row_or_term_index; - int bound_sign = ib.m_is_lower_bound? 1: -1; - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; - unsigned bound_j = ib.m_j; - if (tv::is_term(bound_j)) { - bound_j = m_var_register.external_to_local(bound_j); - } - for (auto const& r : A_r().m_rows[i]) { - unsigned j = r.var(); - if (j == bound_j) continue; - mpq const& a = r.coeff(); - int a_sign = is_pos(a)? 1: -1; - int sign = j_sign * a_sign; - const ul_pair & ul = m_columns_to_ul_pairs[j]; - auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); - lp_assert(is_valid(witness)); - bp.consume(a, witness); - } - // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); -} // here i is just the term index bool lar_solver::term_is_used_as_row(unsigned i) const { SASSERT(i < m_terms.size()); return m_var_register.external_is_used(tv::mask_term(i)); } - -void lar_solver::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); - } -} - -// goes over touched rows and tries to induce bounds -void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { - if (!use_tableau()) - return; // todo: consider to remove the restriction - - 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); - } -} lp_status lar_solver::get_status() const { return m_status; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 6216fafe2..82285a5e6 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -41,8 +41,8 @@ #include "math/lp/conversion_helper.h" #include "math/lp/int_solver.h" #include "math/lp/nra_solver.h" -#include "math/lp/lp_bound_propagator.h" #include "math/lp/lp_types.h" +#include "math/lp/lp_bound_propagator.h" namespace lp { @@ -161,15 +161,53 @@ 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_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, - lp_bound_propagator & bp); + lp_bound_propagator & bp ) { + + if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation + || row_has_a_big_num(row_index)) + return; + lp_assert(use_tableau()); + + bound_analyzer_on_row, lp_bound_propagator>::analyze_row(A_r().m_rows[row_index], + null_ci, + zero_of_type>(), + row_index, + bp + ); + } + void substitute_basis_var_in_terms_for_row(unsigned i); - void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp); - void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset); + 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(); + } static void clean_popped_elements(unsigned n, u_set& set); static void shrink_inf_set_after_pop(unsigned n, u_set & set); bool maximize_term_on_tableau(const lar_term & term, @@ -282,12 +320,55 @@ public: void get_infeasibility_explanation(explanation &) const; inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } - void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp); + template + void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) { + unsigned i = ib.m_row_or_term_index; + int bound_sign = ib.m_is_lower_bound? 1: -1; + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; + unsigned bound_j = ib.m_j; + if (tv::is_term(bound_j)) { + bound_j = m_var_register.external_to_local(bound_j); + } + for (auto const& r : A_r().m_rows[i]) { + unsigned j = r.var(); + if (j == bound_j) continue; + mpq const& a = r.coeff(); + int a_sign = is_pos(a)? 1: -1; + int sign = j_sign * a_sign; + const ul_pair & ul = m_columns_to_ul_pairs[j]; + auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); + lp_assert(is_valid(witness)); + bp.consume(a, witness); + } + } + // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); void activate(constraint_index ci); void random_update(unsigned sz, var_index const * vars); - void propagate_bounds_on_terms(lp_bound_propagator & bp); - void propagate_bounds_for_touched_rows(lp_bound_propagator & bp); + 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 + + 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)); } bool external_is_used(unsigned) const; diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp deleted file mode 100644 index c07a60adb..000000000 --- a/src/math/lp/lp_bound_propagator.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson -*/ -#include "math/lp/lar_solver.h" -namespace lp { -lp_bound_propagator::lp_bound_propagator(lar_solver & ls): - m_lar_solver(ls) {} -column_type lp_bound_propagator::get_column_type(unsigned j) const { - return m_lar_solver.get_column_type(j); -} -const impq & lp_bound_propagator::get_lower_bound(unsigned j) const { - return m_lar_solver.get_lower_bound(j); -} -const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { - return m_lar_solver.get_upper_bound(j); -} -void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { - j = m_lar_solver.adjust_column_index_to_term_index(j); - - lconstraint_kind kind = is_low? GE : LE; - if (strict) - kind = static_cast(kind / 2); - - if (!bound_is_interesting(j, kind, v)) - return; - unsigned k; // index to ibounds - if (is_low) { - if (try_get_value(m_improved_lower_bounds, j, k)) { - auto & found_bound = m_ibounds[k]; - if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); - } - } else { - m_improved_lower_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); - } - } else { // the upper bound case - if (try_get_value(m_improved_upper_bounds, j, k)) { - auto & found_bound = m_ibounds[k]; - if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); - } - } else { - m_improved_upper_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); - } - } -} -} diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9b67162a9..9049b17b2 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -5,24 +5,65 @@ #pragma once #include "math/lp/lp_settings.h" namespace lp { -class lar_solver; +template class lp_bound_propagator { 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; - lar_solver & m_lar_solver; + T& m_imp; public: vector m_ibounds; -public: - lp_bound_propagator(lar_solver & ls); - column_type get_column_type(unsigned) const; - const impq & get_lower_bound(unsigned) const; - const impq & get_upper_bound(unsigned) const; - void try_add_bound(mpq const & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict); - void try_add_eq(lpvar x, lpvar y, unsigned row_or_term_index) {} // TBD - virtual bool bound_is_interesting(unsigned vi, - lp::lconstraint_kind kind, - const rational & bval) {return true;} - unsigned number_of_found_bounds() const { return m_ibounds.size(); } - virtual void consume(mpq const& v, lp::constraint_index j) = 0; + lp_bound_propagator(T& imp): m_imp(imp) {} + column_type get_column_type(unsigned j) const { + return m_imp.lp().get_column_type(j); + } + + const impq & get_lower_bound(unsigned j) const { + return m_imp.lp().get_lower_bound(j); + } + + const impq & get_upper_bound(unsigned j) const { + return m_imp.lp().get_upper_bound(j); + } + + void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { + j = m_imp.lp().adjust_column_index_to_term_index(j); + + lconstraint_kind kind = is_low? GE : LE; + if (strict) + kind = static_cast(kind / 2); + + if (!m_imp.bound_is_interesting(j, kind, v)) + return; + unsigned k; // index to ibounds + if (is_low) { + if (try_get_value(m_improved_lower_bounds, j, k)) { + auto & found_bound = m_ibounds[k]; + if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { + found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } else { + m_improved_lower_bounds[j] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + } + } else { // the upper bound case + if (try_get_value(m_improved_upper_bounds, j, k)) { + auto & found_bound = m_ibounds[k]; + if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { + found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } else { + m_improved_upper_bounds[j] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + } + } + } + + void consume(const mpq& a, constraint_index ci) { + m_imp.consume(a, ci); + } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 659b6cec2..5a966a324 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -328,9 +328,6 @@ class theory_lra::imp { enode* get_enode(expr* e) const { return ctx().get_enode(e); } expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } - lp::lar_solver& lp(){ return *m_solver.get(); } - const lp::lar_solver& lp() const { return *m_solver.get(); } - void init_solver() { if (m_solver) return; @@ -969,6 +966,9 @@ public: std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc()); } + lp::lar_solver& lp(){ return *m_solver.get(); } + const lp::lar_solver& lp() const { return *m_solver.get(); } + void init() { if (m_solver) return; @@ -2311,10 +2311,34 @@ public: // } // } + bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) { + theory_var v = lp().local_to_external(vi); + if (v == null_theory_var) { + return false; + } + if (m_bounds.size() <= static_cast(v) || m_unassigned_bounds[v] == 0) { + return false; + } + for (lp_api::bound* b : m_bounds[v]) { + if (ctx().get_assignment(b->get_bv()) == l_undef && + null_literal != is_bound_implied(kind, bval, *b)) { + return true; + } + } + return false; + } + + void consume(rational const& v, lp::constraint_index j) { + set_evidence(j, m_core, m_eqs); + m_explanation.add_pair(j, v); + } + + void propagate_bounds_with_lp_solver() { if (!should_propagate()) return; - local_bound_propagator bp(*this); + + lp::lp_bound_propagator bp(*this); lp().propagate_bounds_for_touched_rows(bp); @@ -2348,26 +2372,6 @@ public: } return false; } - - struct local_bound_propagator: public lp::lp_bound_propagator { - imp & m_imp; - local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {} - - bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) override { - return m_imp.bound_is_interesting(j, kind, v); - } - - void add_eq(lpvar u, lpvar v, lp::explanation const& e) { - m_imp.add_eq(u, v, e); - } - - void consume(rational const& v, lp::constraint_index j) override { - m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs); - m_imp.m_explanation.add_pair(j, v); - } - }; - - void propagate_lp_solver_bound(lp::implied_bound& be) { lpvar vi = be.m_j; theory_var v = lp().local_to_external(vi); @@ -2400,7 +2404,7 @@ public: first = false; reset_evidence(); m_explanation.clear(); - local_bound_propagator bp(*this); + lp::lp_bound_propagator bp(*this); lp().explain_implied_bound(be, bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); @@ -4024,7 +4028,9 @@ theory_var theory_lra::add_objective(app* term) { expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) { return m_imp->mk_ge(fm, v, val); } - - - } +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&); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index c6e8dbfe7..2522f0e79 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -24,7 +24,9 @@ Revision History: namespace smt { class theory_lra : public theory, public theory_opt { + public: class imp; + private: imp* m_imp; public: diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ae843d59b..9d24d2787 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -313,11 +313,6 @@ void test_cn() { namespace lp { unsigned seed = 1; -class my_bound_propagator : public lp_bound_propagator { -public: - my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls) {} - void consume(mpq const& v, lp::constraint_index j) override {} -}; random_gen g_rand; static unsigned my_random() {