mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

rebase with Z3Prover and Nikolaj's changes in lp bound propagation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-20 15:24:59 -08:00
parent 8388868c27
commit 80245f05ad
3 changed files with 64 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

108
src/math/lp/bound_analyzer_on_row.h
View file

@ -7,7 +7,10 @@ Module Name:
Abstract: Abstract:
<abstract> We have an equality : sum by j of row[j]*x[j] = rs
We try to pin a var by pushing the total by using the variable bounds
on a loop we drive the partial sum down, denoting the variables of this process by _u.
In the same loop trying to pin variables by pushing the partial sum up, denoting the variable related to it by _l
Author: Author:
@ -18,14 +21,12 @@ Revision History:
--*/ --*/
#pragma once #pragma once
#include "util/vector.h" #include "util/vector.h"
#include "implied_bound.h" #include "math/lp/implied_bound.h"
#include "test_bound_analyzer.h"
#include "math/lp/lp_bound_propagator.h" #include "math/lp/lp_bound_propagator.h"
// We have an equality : sum by j of row[j]*x[j] = rs #include "math/lp/test_bound_analyzer.h"
// We try to pin a var by pushing the total by using the variable bounds
// In a loop we drive the partial sum down, denoting the variables of this process by _u.
// In the same loop trying to pin variables by pushing the partial sum up, denoting the variable related to it by _l
namespace lp { namespace lp {
template <typename C> // C plays a role of a container template <typename C> // C plays a role of a container
class bound_analyzer_on_row { class bound_analyzer_on_row {
@ -44,8 +45,7 @@ public :
unsigned bj, // basis column for the row unsigned bj, // basis column for the row
const numeric_pair<mpq>& rs, const numeric_pair<mpq>& rs,
unsigned row_or_term_index, unsigned row_or_term_index,
lp_bound_propagator & bp lp_bound_propagator & bp)
)
: :
m_row(it), m_row(it),
m_bp(bp), m_bp(bp),
@ -56,7 +56,6 @@ public :
{} {}
unsigned j;
void analyze() { void analyze() {
for (const auto & c : m_row) { for (const auto & c : m_row) {
if ((m_column_of_l == -2) && (m_column_of_u == -2)) if ((m_column_of_l == -2) && (m_column_of_u == -2))
@ -80,8 +79,7 @@ public :
} }
bool upper_bound_is_available(unsigned j) const { bool upper_bound_is_available(unsigned j) const {
switch (m_bp.get_column_type(j)) switch (m_bp.get_column_type(j)) {
{
case column_type::fixed: case column_type::fixed:
case column_type::boxed: case column_type::boxed:
case column_type::upper_bound: case column_type::upper_bound:
@ -92,8 +90,7 @@ public :
} }
bool lower_bound_is_available(unsigned j) const { bool lower_bound_is_available(unsigned j) const {
switch (m_bp.get_column_type(j)) switch (m_bp.get_column_type(j)) {
{
case column_type::fixed: case column_type::fixed:
case column_type::boxed: case column_type::boxed:
case column_type::lower_bound: case column_type::lower_bound:
@ -107,12 +104,12 @@ public :
lp_assert(upper_bound_is_available(j)); lp_assert(upper_bound_is_available(j));
return m_bp.get_upper_bound(j); return m_bp.get_upper_bound(j);
} }
const impq & lb(unsigned j) const { const impq & lb(unsigned j) const {
lp_assert(lower_bound_is_available(j)); lp_assert(lower_bound_is_available(j));
return m_bp.get_lower_bound(j); return m_bp.get_lower_bound(j);
} }
const mpq & monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const { const mpq & monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const {
if (a_is_pos) { if (a_is_pos) {
strict = !is_zero(ub(j).y); strict = !is_zero(ub(j).y);
@ -121,12 +118,11 @@ public :
strict = !is_zero(lb(j).y); strict = !is_zero(lb(j).y);
return lb(j).x; return lb(j).x;
} }
mpq monoid_max(const mpq & a, unsigned j) const { mpq monoid_max(const mpq & a, unsigned j) const {
if (is_pos(a)) { return a * (is_pos(a) ? ub(j).x : lb(j).x);
return a * ub(j).x;
}
return a * lb(j).x;
} }
mpq monoid_max(const mpq & a, unsigned j, bool & strict) const { mpq monoid_max(const mpq & a, unsigned j, bool & strict) const {
if (is_pos(a)) { if (is_pos(a)) {
strict = !is_zero(ub(j).y); strict = !is_zero(ub(j).y);
@ -135,6 +131,7 @@ public :
strict = !is_zero(lb(j).y); strict = !is_zero(lb(j).y);
return a * lb(j).x; return a * lb(j).x;
} }
const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const {
if (!a_is_pos) { if (!a_is_pos) {
strict = !is_zero(ub(j).y); strict = !is_zero(ub(j).y);
@ -149,55 +146,48 @@ public :
strict = !is_zero(ub(j).y); strict = !is_zero(ub(j).y);
return a * ub(j).x; return a * ub(j).x;
} }
strict = !is_zero(lb(j).y); strict = !is_zero(lb(j).y);
return a * lb(j).x; return a * lb(j).x;
} }
mpq monoid_min(const mpq & a, unsigned j) const { mpq monoid_min(const mpq & a, unsigned j) const {
if (is_neg(a)) { return a * (is_neg(a) ? ub(j).x : lb(j).x);
return a * ub(j).x;
} }
return a * lb(j).x; mpq m_total, m_bound;
}
void limit_all_monoids_from_above() { void limit_all_monoids_from_above() {
int strict = 0; int strict = 0;
mpq total; m_total.reset();
lp_assert(is_zero(total)); lp_assert(is_zero(total));
for (const auto& p : m_row) { for (const auto& p : m_row) {
bool str; bool str;
total -= monoid_min(p.coeff(), p.var(), str); m_total -= monoid_min(p.coeff(), p.var(), str);
if (str) if (str)
strict++; strict++;
} }
mpq bound;
for (const auto &p : m_row) { for (const auto &p : m_row) {
bool str; bool str;
bool a_is_pos = is_pos(p.coeff()); bool a_is_pos = is_pos(p.coeff());
bound = total; m_bound = m_total;
bound /= p.coeff(); m_bound /= p.coeff();
bound += monoid_min_no_mult(a_is_pos, p.var(), str); m_bound += monoid_min_no_mult(a_is_pos, p.var(), str);
if (a_is_pos) { if (a_is_pos) {
limit_j(p.var(), bound, true, false, strict - static_cast<int>(str) > 0); limit_j(p.var(), m_bound, true, false, strict - static_cast<int>(str) > 0);
} }
else { else {
limit_j(p.var(), bound, false, true, strict - static_cast<int>(str) > 0); limit_j(p.var(), m_bound, false, true, strict - static_cast<int>(str) > 0);
} }
} }
} }
void limit_all_monoids_from_below() { void limit_all_monoids_from_below() {
int strict = 0; int strict = 0;
mpq total; m_total.reset();
lp_assert(is_zero(total)); lp_assert(is_zero(total));
for (const auto &p : m_row) { for (const auto &p : m_row) {
bool str; bool str;
total -= monoid_max(p.coeff(), p.var(), str); m_total -= monoid_max(p.coeff(), p.var(), str);
if (str) if (str)
strict++; strict++;
} }
@ -205,13 +195,15 @@ public :
for (const auto& p : m_row) { for (const auto& p : m_row) {
bool str; bool str;
bool a_is_pos = is_pos(p.coeff()); bool a_is_pos = is_pos(p.coeff());
mpq bound = total / p.coeff() + monoid_max_no_mult(a_is_pos, p.var(), str); m_bound = m_total;
m_bound /= p.coeff();
m_bound += monoid_max_no_mult(a_is_pos, p.var(), str);
bool astrict = strict - static_cast<int>(str) > 0; bool astrict = strict - static_cast<int>(str) > 0;
if (a_is_pos) { if (a_is_pos) {
limit_j(p.var(), bound, true, true, astrict); limit_j(p.var(), m_bound, true, true, astrict);
} }
else { else {
limit_j(p.var(), bound, false, false, astrict); limit_j(p.var(), m_bound, false, false, astrict);
} }
} }
} }
@ -222,7 +214,7 @@ public :
// every other monoid is impossible to limit from below // every other monoid is impossible to limit from below
mpq u_coeff; mpq u_coeff;
unsigned j; unsigned j;
mpq bound = -m_rs.x; m_bound = -m_rs.x;
bool strict = false; bool strict = false;
for (const auto& p : m_row) { for (const auto& p : m_row) {
j = p.var(); j = p.var();
@ -231,17 +223,17 @@ public :
continue; continue;
} }
bool str; bool str;
bound -= monoid_max(p.coeff(), j, str); m_bound -= monoid_max(p.coeff(), j, str);
if (str) if (str)
strict = true; strict = true;
} }
bound /= u_coeff; m_bound /= u_coeff;
if (u_coeff.is_pos()) { if (u_coeff.is_pos()) {
limit_j(m_column_of_u, bound, true, true, strict); limit_j(m_column_of_u, m_bound, true, true, strict);
} else { } else {
limit_j(m_column_of_u, bound, false, false, strict); limit_j(m_column_of_u, m_bound, false, false, strict);
} }
} }
@ -251,7 +243,7 @@ public :
// every other monoid is impossible to limit from above // every other monoid is impossible to limit from above
mpq l_coeff; mpq l_coeff;
unsigned j; unsigned j;
mpq bound = -m_rs.x; m_bound = -m_rs.x;
bool strict = false; bool strict = false;
for (const auto &p : m_row) { for (const auto &p : m_row) {
j = p.var(); j = p.var();
@ -261,15 +253,15 @@ public :
} }
bool str; bool str;
bound -= monoid_min(p.coeff(), j, str); m_bound -= monoid_min(p.coeff(), j, str);
if (str) if (str)
strict = true; strict = true;
} }
bound /= l_coeff; m_bound /= l_coeff;
if (is_pos(l_coeff)) { if (is_pos(l_coeff)) {
limit_j(m_column_of_l, bound, true, false, strict); limit_j(m_column_of_l, m_bound, true, false, strict);
} else { } else {
limit_j(m_column_of_l, bound, false, true, strict); limit_j(m_column_of_l, m_bound, false, true, strict);
} }
} }
@ -296,19 +288,12 @@ public :
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_or_term_index, strict);
} }
void advance_u(unsigned j) { void advance_u(unsigned j) {
if (m_column_of_u == -1) m_column_of_u = (m_column_of_u == -1) ? j : -2;
m_column_of_u = j;
else
m_column_of_u = -2;
} }
void advance_l(unsigned j) { void advance_l(unsigned j) {
if (m_column_of_l == -1) m_column_of_l = (m_column_of_l == -1) ? j : -2;
m_column_of_l = j;
else
m_column_of_l = -2;
} }
void analyze_bound_on_var_on_coeff(int j, const mpq &a) { void analyze_bound_on_var_on_coeff(int j, const mpq &a) {
@ -320,7 +305,7 @@ public :
advance_l(j); advance_l(j);
break; break;
case column_type::upper_bound: case column_type::upper_bound:
if(numeric_traits<mpq>::is_neg(a)) if (numeric_traits<mpq>::is_neg(a))
advance_u(j); advance_u(j);
else else
advance_l(j); advance_l(j);
@ -338,8 +323,7 @@ public :
unsigned bj, // basis column for the row unsigned bj, // basis column for the row
const numeric_pair<mpq>& rs, const numeric_pair<mpq>& rs,
unsigned row_or_term_index, unsigned row_or_term_index,
lp_bound_propagator & bp lp_bound_propagator & 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();
} }

2
src/math/lp/lp_bound_propagator.cpp
View file

@ -15,7 +15,7 @@ const impq & lp_bound_propagator::get_lower_bound(unsigned j) const {
const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { const impq & lp_bound_propagator::get_upper_bound(unsigned j) const {
return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
} }
void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { 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); j = m_lar_solver.adjust_column_index_to_term_index(j);
lconstraint_kind kind = is_low? GE : LE; lconstraint_kind kind = is_low? GE : LE;

2
src/math/lp/lp_bound_propagator.h
View file

@ -17,7 +17,7 @@ public:
column_type get_column_type(unsigned) const; column_type get_column_type(unsigned) const;
const impq & get_lower_bound(unsigned) const; const impq & get_lower_bound(unsigned) const;
const impq & get_upper_bound(unsigned) const; const impq & get_upper_bound(unsigned) const;
void try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict); 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);
virtual bool bound_is_interesting(unsigned vi, virtual bool bound_is_interesting(unsigned vi,
lp::lconstraint_kind kind, lp::lconstraint_kind kind,
const rational & bval) {return true;} const rational & bval) {return true;}