mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

use static_cast to avoid the warnings

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-13 07:07:12 -10:00
parent e6a089e63d
commit bedc95c4c7
8 changed files with 30 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/dioph_eq.cpp
View file

@ -2014,7 +2014,10 @@ namespace lp {
}
unsigned get_markovich_number(unsigned k, unsigned h) {
return (m_e_matrix.m_columns[k].size() - 1) * (m_e_matrix.m_rows[h].size() - 1);
size_t col_size = m_e_matrix.m_columns[k].size();
size_t row_size = m_e_matrix.m_rows[h].size();
// Subtract 1 from sizes once and multiply
return static_cast<unsigned>((col_size - 1) * (row_size - 1));
}
std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) {

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

@ -1371,7 +1371,7 @@ namespace lp {
lp_assert(A_r().row_count() == i + 1 && A_r().column_count() == j + 1);
auto& last_column = A_r().m_columns[j];
int non_zero_column_cell_index = -1;
for (unsigned k = last_column.size(); k-- > 0;) {
for (unsigned k = static_cast<unsigned>(last_column.size()); k-- > 0;) {
auto& cc = last_column[k];
if (cc.var() == i)
return;
@ -1395,7 +1395,7 @@ namespace lp {
auto& last_row = A_r().m_rows[i];
mpq& cost_j = m_mpq_lar_core_solver.m_r_solver.m_costs[j];
bool cost_is_nz = !is_zero(cost_j);
for (unsigned k = last_row.size(); k-- > 0;) {
for (unsigned k = static_cast<unsigned>(last_row.size()); k-- > 0;) {
auto& rc = last_row[k];
if (cost_is_nz) {
m_mpq_lar_core_solver.m_r_solver.m_d[rc.var()] += cost_j * rc.coeff();

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

@ -347,7 +347,7 @@ public:
void init_non_basic_part_of_basis_heading() {
this->m_nbasis.clear();
for (int j = m_basis_heading.size(); j--;){
for (unsigned j = static_cast<unsigned>(m_basis_heading.size()); j--;){
if (m_basis_heading[j] < 0) {
m_nbasis.push_back(j);
// the index of column j in m_nbasis is (- basis_heading[j] - 1)

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

@ -225,7 +225,7 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::
divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
int pivot_index = -1;
auto & row = m_A.m_rows[pivot_row];
unsigned size = row.size();
unsigned size = static_cast<unsigned>(row.size());
for (unsigned j = 0; j < size; j++) {
auto & c = row[j];
if (c.var() == pivot_col) {

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

@ -208,10 +208,10 @@ namespace lp {
continue;
}
unsigned not_free = get_num_of_not_free_basic_dependent_vars(j, min_non_free_so_far, bj);
unsigned col_sz = this->m_A.m_columns[j].size();
unsigned col_sz = static_cast<unsigned>(this->m_A.m_columns[j].size());
if (not_free < min_non_free_so_far || (not_free == min_non_free_so_far && col_sz < best_col_sz)) {
min_non_free_so_far = not_free;
best_col_sz = this->m_A.m_columns[j].size();
best_col_sz = static_cast<unsigned>(this->m_A.m_columns[j].size());
choice = k;
nchoices = 1;
}

8
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -201,7 +201,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
unsigned row_min_nz = this->m_n() + 1;
m_leaving_candidates.clear();
auto & col = this->m_A.m_columns[entering];
unsigned col_size = col.size();
unsigned col_size = static_cast<unsigned>(col.size());
for (;k < col_size && unlimited; k++) {
const column_cell & c = col[k];
unsigned i = c.var();
@ -211,7 +211,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
limit_theta_on_basis_column(j, - ed * m_sign_of_entering_delta, t, unlimited);
if (!unlimited) {
m_leaving_candidates.push_back(j);
row_min_nz = this->m_A.m_rows[i].size();
row_min_nz = static_cast<unsigned>(this->m_A.m_rows[i].size());
}
}
if (unlimited) {
@ -230,7 +230,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
unlimited = true;
limit_theta_on_basis_column(j, -ed * m_sign_of_entering_delta, ratio, unlimited);
if (unlimited) continue;
unsigned i_nz = this->m_A.m_rows[i].size();
unsigned i_nz = static_cast<unsigned>(this->m_A.m_rows[i].size());
if (ratio < t) {
t = ratio;
m_leaving_candidates.clear();
@ -239,7 +239,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
} else if (ratio == t && i_nz < row_min_nz) {
m_leaving_candidates.clear();
m_leaving_candidates.push_back(j);
row_min_nz = this->m_A.m_rows[i].size();
row_min_nz = static_cast<unsigned>(this->m_A.m_rows[i].size());
} else if (ratio == t && i_nz == row_min_nz) {
m_leaving_candidates.push_back(j);
}

6
src/math/lp/static_matrix.h
View file

@ -2,9 +2,7 @@
Copyright (c) 2017 Microsoft Corporation
Author:
Lev Nachmanson (levnach)
--*/
#pragma once
@ -204,7 +202,7 @@ public:
T get_elem(unsigned i, unsigned j) const;
unsigned number_of_non_zeroes_in_column(unsigned j) const { return m_columns[j].size(); }
unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast<unsigned>(m_columns[j].size()); }
unsigned number_of_non_zeroes_in_row(unsigned i) const { return m_rows[i].size(); }
@ -257,7 +255,7 @@ public:
if (m_stack.empty()) break;
unsigned m = m_stack.top().m_m;
while (m < row_count()) {
unsigned i = m_rows.size() -1 ;
unsigned i = static_cast<unsigned>(m_rows.size() -1);
auto & row = m_rows[i];
pop_row_columns(row);
m_rows.pop_back(); // delete the last row

28
src/math/lp/static_matrix_def.h
View file

@ -57,7 +57,7 @@ namespace lp {
auto & rowii = m_rows[ii];
remove_element(rowii, rowii[c.offset()]);
scan_row_strip_to_work_vector(rowii);
unsigned prev_size_ii = rowii.size();
unsigned prev_size_ii = static_cast<unsigned>(rowii.size());
// run over the pivot row and update row ii
for (const auto & iv : m_rows[i]) {
unsigned j = iv.var();
@ -78,7 +78,7 @@ namespace lp {
}
// remove zeroes
for (unsigned k = rowii.size(); k-- > 0; ) {
for (unsigned k = static_cast<unsigned>(rowii.size()); k-- > 0; ) {
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
@ -90,7 +90,7 @@ namespace lp {
lp_assert(i < row_count() && k < row_count() && i != k);
auto & rowk = m_rows[k];
scan_row_strip_to_work_vector(rowk);
unsigned prev_size_k = rowk.size();
unsigned prev_size_k = static_cast<unsigned>(rowk.size());
// run over the pivot row and update row k
for (const auto & iv : m_rows[i]) {
unsigned j = iv.var();
@ -109,7 +109,7 @@ namespace lp {
}
// remove zeroes
for (unsigned k = rowk.size(); k-- > 0; ) {
for (unsigned k = static_cast<unsigned>(rowk.size()); k-- > 0; ) {
if (is_zero(rowk[k].coeff()))
remove_element(rowk, rowk[k]);
}
@ -126,7 +126,7 @@ namespace lp {
auto & rowii = m_rows[ii];
remove_element(rowii, rowii[c.offset()]);
scan_row_strip_to_work_vector(rowii);
unsigned prev_size_ii = rowii.size();
unsigned prev_size_ii = static_cast<unsigned>(rowii.size());
// run over the pivot row and update row ii
for (const auto & iv : m_rows[piv_row_index]) {
unsigned j = iv.var();
@ -147,7 +147,7 @@ namespace lp {
}
// remove zeroes
for (unsigned k = rowii.size(); k-- > 0; ) {
for (unsigned k = static_cast<unsigned>(rowii.size()); k-- > 0; ) {
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
@ -159,7 +159,7 @@ namespace lp {
void static_matrix<T, X>::add_term_to_row(const mpq& alpha, TTerm const & term, unsigned ii) {
auto & rowii = m_rows[ii];
scan_row_strip_to_work_vector(rowii);
unsigned prev_size_ii = rowii.size();
unsigned prev_size_ii = static_cast<unsigned>(rowii.size());
// run over the term and update row ii
for (const auto & iv : term) {
unsigned j = iv.var();
@ -180,7 +180,7 @@ namespace lp {
}
// remove zeroes
for (unsigned k = rowii.size(); k-- > 0; ) {
for (unsigned k = static_cast<unsigned>(rowii.size()); k-- > 0; ) {
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
@ -195,7 +195,7 @@ namespace lp {
auto & rowii = m_rows[ii];
remove_element(rowii, rowii[c.offset()]);
scan_row_strip_to_work_vector(rowii);
unsigned prev_size_ii = rowii.size();
unsigned prev_size_ii = static_cast<unsigned>(rowii.size());
// run over the pivot row and update row ii
for (const auto & iv : term) {
unsigned j = iv.var();
@ -216,7 +216,7 @@ namespace lp {
}
// remove zeroes
for (unsigned k = rowii.size(); k-- > 0; ) {
for (unsigned k = static_cast<unsigned>(rowii.size()); k-- > 0; ) {
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
@ -257,8 +257,8 @@ namespace lp {
if (numeric_traits<T>::is_zero(val)) return;
SASSERT(row < row_count() && col < column_count());
auto & r = m_rows[row];
unsigned offs_in_cols = m_columns[col].size();
m_columns[col].push_back(make_column_cell(row, r.size()));
unsigned offs_in_cols = static_cast<unsigned>(m_columns[col].size());
m_columns[col].push_back(make_column_cell(row, static_cast<unsigned>(r.size())));
r.push_back(make_row_cell(col, offs_in_cols, val));
}
@ -479,8 +479,8 @@ namespace lp {
void static_matrix<T, X>::add_new_element(unsigned row, unsigned col, const T& val) {
auto & row_vals = m_rows[row];
auto & col_vals = m_columns[col];
unsigned row_el_offs = row_vals.size();
unsigned col_el_offs = col_vals.size();
unsigned row_el_offs = static_cast<unsigned>(row_vals.size());
unsigned col_el_offs = static_cast<unsigned>(col_vals.size());
row_vals.push_back(row_cell<T>(col, col_el_offs, val));
col_vals.push_back(column_cell(row, row_el_offs));
}