From cbad61ba2e157b86abaf03dfb4db0d3c912f5988 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 13 Sep 2023 14:27:34 -0700 Subject: [PATCH] propagate monics with lp_bound_propagator --- src/math/lp/bound_analyzer_on_row.h | 43 ++++------------- src/math/lp/implied_bound.h | 16 ++++-- src/math/lp/lar_solver.h | 2 +- src/math/lp/lp_bound_propagator.h | 75 ++++++++++++++++++++--------- src/sat/smt/arith_solver.cpp | 2 +- 5 files changed, 74 insertions(+), 64 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 35e3bb6ed..5af864220 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -93,39 +93,17 @@ private: } bool bound_is_available(unsigned j, bool lower_bound) { - return (lower_bound && lower_bound_is_available(j)) || - (!lower_bound && upper_bound_is_available(j)); - } - - bool upper_bound_is_available(unsigned j) const { - switch (m_bp.get_column_type(j)) { - case column_type::fixed: - case column_type::boxed: - case column_type::upper_bound: - return true; - default: - return false; - } - } - - bool lower_bound_is_available(unsigned j) const { - switch (m_bp.get_column_type(j)) { - case column_type::fixed: - case column_type::boxed: - case column_type::lower_bound: - return true; - default: - return false; - } + return (lower_bound && m_bp.lower_bound_is_available(j)) || + (!lower_bound && m_bp.upper_bound_is_available(j)); } const impq & ub(unsigned j) const { - lp_assert(upper_bound_is_available(j)); + lp_assert(m_bp.upper_bound_is_available(j)); return m_bp.get_upper_bound(j); } const impq & lb(unsigned j) const { - lp_assert(lower_bound_is_available(j)); + lp_assert(m_bp.lower_bound_is_available(j)); return m_bp.get_lower_bound(j); } @@ -305,9 +283,8 @@ private: void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ - lar_solver* lar = & this->m_bp.lp(); unsigned row_index = this->m_row_index; - auto explain = [lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index]() { return explain_bound_on_var_on_coeff(lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); }; + auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index](lar_solver& s) { return explain_bound_on_var_on_coeff(s, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); }; m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain ); } @@ -341,22 +318,22 @@ private: break; } } - static u_dependency* explain_bound_on_var_on_coeff(lar_solver* lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { + static u_dependency* explain_bound_on_var_on_coeff(lar_solver& lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { int bound_sign = (is_lower_bound ? 1 : -1); int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; if (tv::is_term(bound_j)) - bound_j = lar->map_term_index_to_column_index(bound_j); + bound_j = lar.map_term_index_to_column_index(bound_j); u_dependency* ret = nullptr; - for (auto const& r : lar->get_row(row_index)) { + for (auto const& r : lar.get_row(row_index)) { 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; - u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j); - ret = lar->join_deps(ret, witness); + u_dependency* witness = sign > 0 ? lar.get_column_upper_bound_witness(j) : lar.get_column_lower_bound_witness(j); + ret = lar.join_deps(ret, witness); } return ret; } diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h index 2e7fcbbcb..0df1f4f60 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -20,18 +20,24 @@ Revision History: #pragma once #include "math/lp/lp_settings.h" #include "math/lp/lar_constraints.h" +#include "math/lp/lar_solver.h" namespace lp { class implied_bound { public: mpq m_bound; - unsigned m_j; // the column for which the bound has been found + // It is either the column for which the bound has been found, or, + // in the case the column was created as + // the slack variable to a term, it is the term index. + // It is the same index that was returned by lar_solver::add_var(), or + // by lar_solver::add_term() + unsigned m_j; bool m_is_lower_bound; bool m_strict; private: - std::function m_explain_bound = nullptr; + std::function m_explain_bound = nullptr; public: - u_dependency* explain() const { return m_explain_bound(); } - void set_explain(std::function f) { m_explain_bound = f; } + u_dependency* explain(lar_solver& s) const { return m_explain_bound(s); } + void set_explain(std::function f) { m_explain_bound = f; } lconstraint_kind kind() const { lconstraint_kind k = m_is_lower_bound? GE : LE; if (m_strict) @@ -43,7 +49,7 @@ class implied_bound { unsigned j, bool is_lower_bound, bool is_strict, - std::function get_dep): + std::function get_dep): m_bound(a), m_j(j), m_is_lower_bound(is_lower_bound), diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 7d16c7b63..50e9de7a3 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -311,7 +311,7 @@ class lar_solver : public column_namer { template void explain_implied_bound(const implied_bound& ib, lp_bound_propagator& bp) { - u_dependency* dep = ib.explain(); + u_dependency* dep = ib.explain(*this); for (auto ci : flatten(dep)) bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients /* diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 7ee647200..c67e99651 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -39,8 +39,28 @@ class lp_bound_propagator { } return x != UINT_MAX; } - - +public: + bool upper_bound_is_available(unsigned j) const { + switch (get_column_type(j)) { + case column_type::fixed: + case column_type::boxed: + case column_type::upper_bound: + return true; + default: + return false; + } + } + bool lower_bound_is_available(unsigned j) const { + switch (get_column_type(j)) { + case column_type::fixed: + case column_type::boxed: + case column_type::lower_bound: + return true; + default: + return false; + } + } +private: void try_add_equation_with_internal_fixed_tables(unsigned r1) { unsigned v1, v2; if (!only_one_nfixed(r1, v1)) @@ -119,11 +139,11 @@ class lp_bound_propagator { } void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { - add_lower_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);}); - add_upper_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);}); + add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); + add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); } - void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function explain_dep) { + void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function explain_dep) { unsigned k; if (!try_get_value(m_improved_lower_bounds, monic_var, k)) { m_improved_lower_bounds[monic_var] = m_ibounds.size(); @@ -137,7 +157,7 @@ class lp_bound_propagator { } } - void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function explain_bound) { + void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function explain_bound) { unsigned k; if (!try_get_value(m_improved_upper_bounds, monic_var, k)) { m_improved_upper_bounds[monic_var] = m_ibounds.size(); @@ -160,47 +180,54 @@ class lp_bound_propagator { if (zero_var != null_lpvar) { add_bounds_for_zero_var(monic_var, zero_var); } else { - if (non_fixed != null_lpvar && get_column_type(non_fixed) == column_type::free_column) return; rational k = rational(1); for (auto v : vars) if (v != non_fixed) { k *= lp().get_column_value(v).x; if (k.is_big()) return; } - u_dependency* dep; - lp::mpq bound_value; + lp::impq bound_value; bool is_strict; if (non_fixed != null_lpvar) { - if (this->lp().has_lower_bound(non_fixed, dep, bound_value, is_strict)) { + if (lower_bound_is_available(non_fixed)) { + bound_value = lp().column_lower_bound(non_fixed); + is_strict = !bound_value.y.is_zero(); if (k.is_pos()) - add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() { return dep; }); + add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](lar_solver& s) { return s.get_column_lower_bound_witness(non_fixed); }); else - add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_lower_bound_witness(non_fixed);}); } - if (this->lp().has_upper_bound(non_fixed, dep, bound_value, is_strict)) { + if (upper_bound_is_available(non_fixed)) { + bound_value = lp().column_upper_bound(non_fixed); + is_strict = !bound_value.y.is_zero(); if (k.is_neg()) - add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); else - add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); } - if (this->lp().has_lower_bound(monic_var, dep, bound_value, is_strict)) { + if (lower_bound_is_available(monic_var)) { + bound_value = lp().column_lower_bound(monic_var); + is_strict = !bound_value.y.is_zero(); if (k.is_pos()) - add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_lower_bound_witness(monic_var);}); else - add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_lower_bound_witness(monic_var);}); } - if (this->lp().has_upper_bound(monic_var, dep, bound_value, is_strict)) { + if (upper_bound_is_available(monic_var)) { + bound_value = lp().column_upper_bound(monic_var); + is_strict = !bound_value.y.is_zero(); if (k.is_neg()) - add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_upper_bound_witness(monic_var);}); else - add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_upper_bound_witness(monic_var);}); } + } else { // all variables are fixed - add_lower_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);}); - add_upper_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);}); + add_lower_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); + add_upper_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); } } } @@ -233,7 +260,7 @@ class lp_bound_propagator { return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero(); } - void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { + void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { j = m_imp.lp().column_to_reported_index(j); lconstraint_kind kind = is_low ? GE : LE; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index e4bec83cc..346fbb7a9 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -253,7 +253,7 @@ namespace arith { first = false; reset_evidence(); m_explanation.clear(); - be.explain(); + be.explain(lp()); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1);