From e5632736d234bc1af6c43dc6f08f1837b976474d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 12 Jun 2020 18:08:26 -0700 Subject: [PATCH] review comments Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 2 +- src/math/lp/lar_solver.cpp | 8 ++++---- src/math/lp/lp_bound_propagator.h | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index e93aea3fe..38ea9e10b 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -340,7 +340,7 @@ private: m_bp.cheap_eq_table(m_row_index); break; default: - UNREACHABLE(); + return; } } }; diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 7714f54ce..965e9acc7 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1732,7 +1732,7 @@ void lar_solver::remove_non_fixed_from_fixed_var_table() { vector to_remove; for (const auto& p : m_fixed_var_table) { unsigned j = p.m_value; - if (j >= column_count() || column_is_fixed(j) == false) + if (j >= column_count() || !column_is_fixed(j)) to_remove.push_back(p.m_key); } for (const auto & p : to_remove) @@ -1748,7 +1748,7 @@ void lar_solver::register_in_fixed_var_table(unsigned j, unsigned & equal_to_j) value_sort_pair key(bound.x, column_is_int(j)); unsigned k; - if (m_fixed_var_table.find(key, k) == false ) { + if (!m_fixed_var_table.find(key, k)) { m_fixed_var_table.insert(key, j); return; } @@ -2189,7 +2189,7 @@ bool lar_solver::tighten_term_bounds_by_delta(tv const& t, const impq& delta) { SASSERT(t.is_term()); unsigned tj = t.index(); unsigned j; - if (m_var_register.external_is_used(tj, j) == false) + if (!m_var_register.external_is_used(tj, j)) return true; // the term is not a column so it has no bounds auto & slv = m_mpq_lar_core_solver.m_r_solver; TRACE("cube", tout << "delta = " << delta << std::endl; @@ -2279,7 +2279,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, lp_assert(t.is_term()) unsigned j; bool is_int; - if (m_var_register.external_is_used(t.index(), j, is_int) == false) + if (!m_var_register.external_is_used(t.index(), j, is_int)) return false; // the term does not have a bound because it does not correspond to a column if (!is_int) // todo - allow for the next version of hnf return false; diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index bbc701817..a2a5efbdf 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -117,7 +117,7 @@ public: 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)) { + 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); TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); } @@ -129,7 +129,7 @@ public: } 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)) { + 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); TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); }