mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

review comments

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-12 18:08:26 -07:00
parent fbfcc6796a
commit e5632736d2
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -340,7 +340,7 @@ private:
m_bp.cheap_eq_table(m_row_index); m_bp.cheap_eq_table(m_row_index);
break; break;
default: default:
UNREACHABLE(); return;
} }
} }
}; };

8
src/math/lp/lar_solver.cpp
View file

@ -1732,7 +1732,7 @@ void lar_solver::remove_non_fixed_from_fixed_var_table() {
vector<value_sort_pair> to_remove; vector<value_sort_pair> to_remove;
for (const auto& p : m_fixed_var_table) { for (const auto& p : m_fixed_var_table) {
unsigned j = p.m_value; 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); to_remove.push_back(p.m_key);
} }
for (const auto & p : to_remove) 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)); value_sort_pair key(bound.x, column_is_int(j));
unsigned k; 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); m_fixed_var_table.insert(key, j);
return; return;
} }
@ -2189,7 +2189,7 @@ bool lar_solver::tighten_term_bounds_by_delta(tv const& t, const impq& delta) {
SASSERT(t.is_term()); SASSERT(t.is_term());
unsigned tj = t.index(); unsigned tj = t.index();
unsigned j; 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 return true; // the term is not a column so it has no bounds
auto & slv = m_mpq_lar_core_solver.m_r_solver; auto & slv = m_mpq_lar_core_solver.m_r_solver;
TRACE("cube", tout << "delta = " << delta << std::endl; 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()) lp_assert(t.is_term())
unsigned j; unsigned j;
bool is_int; 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 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 if (!is_int) // todo - allow for the next version of hnf
return false; return false;

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

@ -117,7 +117,7 @@ public:
if (is_low) { if (is_low) {
if (try_get_value(m_improved_lower_bounds, j, k)) { if (try_get_value(m_improved_lower_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 == 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); 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", m_imp.lp().print_implied_bound(found_bound, tout););
} }
@ -129,7 +129,7 @@ public:
} 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 == 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); 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", m_imp.lp().print_implied_bound(found_bound, tout););
} }