mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

port over cosmetics from unit_prop_on_monomials branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-26 20:24:49 -07:00
parent 36566d6193
commit 9c63ea3135
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -103,19 +103,19 @@ class lp_bound_propagator {
} }
const impq& get_lower_bound(unsigned j) const { const impq& get_lower_bound(unsigned j) const {
return m_imp.lp().get_lower_bound(j); return lp().get_lower_bound(j);
} }
const mpq& get_lower_bound_rational(unsigned j) const { const mpq& get_lower_bound_rational(unsigned j) const {
return m_imp.lp().get_lower_bound(j).x; return lp().get_lower_bound(j).x;
} }
const impq& get_upper_bound(unsigned j) const { const impq& get_upper_bound(unsigned j) const {
return m_imp.lp().get_upper_bound(j); return lp().get_upper_bound(j);
} }
const mpq& get_upper_bound_rational(unsigned j) const { const mpq& get_upper_bound_rational(unsigned j) const {
return m_imp.lp().get_upper_bound(j).x; return lp().get_upper_bound(j).x;
} }
// require also the zero infinitesemal part // require also the zero infinitesemal part
@ -124,7 +124,7 @@ class lp_bound_propagator {
} }
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_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().column_to_reported_index(j); j = lp().column_to_reported_index(j);
lconstraint_kind kind = is_low ? GE : LE; lconstraint_kind kind = is_low ? GE : LE;
if (strict) if (strict)
@ -138,24 +138,24 @@ class lp_bound_propagator {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, 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);); TRACE("try_add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_lower_bounds[j] = m_ibounds.size(); 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)); 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);); TRACE("try_add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }
} else { // the upper bound case } else { // the upper bound case
if (try_get_value(m_improved_upper_bounds, j, k)) { if (try_get_value(m_improved_upper_bounds, j, k)) {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, 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);); TRACE("try_add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_upper_bounds[j] = m_ibounds.size(); 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)); 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);); TRACE("try_add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }
} }
} }