mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

before getting explanations for monomials upper and low bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-06 17:09:10 -07:00
parent 6a6cb3822c
commit 70824a68b6
2 changed files with 48 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -50,16 +50,23 @@ bool lp_bound_propagator::upper_bound_is_available(unsigned j) const {
return false; return false;
return m_nla_solver->monomial_has_upper_bound(j); return m_nla_solver->monomial_has_upper_bound(j);
} }
bool lp_bound_propagator::nl_monomial_upper_bound_is_available(unsigned j) const {
return m_nla_solver && m_nla_solver->is_monomial_var(j)
&&
m_nla_solver->monomial_has_upper_bound(j);
}
bool lp_bound_propagator::nl_monomial_lower_bound_is_available(unsigned j) const {
return m_nla_solver && m_nla_solver->is_monomial_var(j)
&&
m_nla_solver->monomial_has_lower_bound(j);
}
impq lp_bound_propagator::get_lower_bound(unsigned j) const { impq lp_bound_propagator::get_lower_bound(unsigned j) const {
lp_assert(lower_bound_is_available(j)); lp_assert(lower_bound_is_available(j));
if (lower_bound_is_available_for_column(j)) { if (lower_bound_is_available_for_column(j)) {
const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]; const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j];
if (!(m_nla_solver && m_nla_solver->is_monomial_var(j))) return nl_monomial_lower_bound_is_available(j)?
return l; std::max(l, m_nla_solver->get_lower_bound(j)) : l;
if (m_nla_solver->monomial_has_lower_bound(j))
return std::max(l, m_nla_solver->get_lower_bound(j));
return l;
} }
return m_nla_solver->get_lower_bound(j); return m_nla_solver->get_lower_bound(j);
} }
@ -68,11 +75,8 @@ impq lp_bound_propagator::get_upper_bound(unsigned j) const {
lp_assert(upper_bound_is_available(j)); lp_assert(upper_bound_is_available(j));
if (upper_bound_is_available_for_column(j)) { if (upper_bound_is_available_for_column(j)) {
const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
if (!(m_nla_solver && m_nla_solver->is_monomial_var(j))) return nl_monomial_upper_bound_is_available(j)?
return l; std::min(l, m_nla_solver->get_upper_bound(j)) : l;
if (m_nla_solver->monomial_has_upper_bound(j))
return std::min(l, m_nla_solver->get_upper_bound(j));
return l;
} }
return m_nla_solver->get_upper_bound(j); return m_nla_solver->get_upper_bound(j);
} }
@ -114,6 +118,15 @@ void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool co
} }
} }
} }
bool lp_bound_propagator::nl_monomial_upper_bound_should_be_taken(unsigned j) const {
return (!upper_bound_is_available_for_column(j)) || (
nl_monomial_upper_bound_is_available(j) && m_nla_solver->get_lower_bound(j) < m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]);
}
bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const {
return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]);
}
void lp_bound_propagator::explain_implied_bound(implied_bound & ib) { void lp_bound_propagator::explain_implied_bound(implied_bound & ib) {
unsigned i = ib.m_row_or_term_index; unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1; int bound_sign = ib.m_is_lower_bound? 1: -1;
@ -128,14 +141,26 @@ void lp_bound_propagator::explain_implied_bound(implied_bound & ib) {
mpq const& a = r.get_val(); mpq const& a = r.get_val();
int a_sign = is_pos(a)? 1: -1; int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign; int sign = j_sign * a_sign;
if (sign > 0) {
if (nl_monomial_upper_bound_should_be_taken(j)) {
SASSERT(false);
} else {
const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j]; const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j];
// todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!! auto witness = ul.upper_bound_witness();
auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
lp_assert(is_valid(witness)); lp_assert(is_valid(witness));
consume(a, witness); consume(a, witness);
} }
// lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } else {
if (nl_monomial_lower_bound_should_be_taken(j)) {
SASSERT(false);
} else {
const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j];
// todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
auto witness = ul.lower_bound_witness();
lp_assert(is_valid(witness));
consume(a, witness);
} }
} }
}
}
} // end of namespace lp

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

@ -34,5 +34,9 @@ public:
unsigned number_of_found_bounds() const { return m_ibounds.size(); } unsigned number_of_found_bounds() const { return m_ibounds.size(); }
void explain_implied_bound(implied_bound & ib); void explain_implied_bound(implied_bound & ib);
virtual void consume(mpq const& v, lp::constraint_index j) = 0; virtual void consume(mpq const& v, lp::constraint_index j) = 0;
bool nl_monomial_upper_bound_is_available(unsigned) const;
bool nl_monomial_lower_bound_is_available(unsigned) const;
bool nl_monomial_lower_bound_should_be_taken(unsigned) const;
bool nl_monomial_upper_bound_should_be_taken(unsigned) const;
}; };
} }