use static_cast to avoid the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/dioph_eq.cpp

@@ -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) {

src/math/lp/lar_solver.cpp

@@ -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();

src/math/lp/lp_core_solver_base.h

@@ -347,7 +347,7 @@ class lp_core_solver_base {
 
     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)

src/math/lp/lp_core_solver_base_def.h

@@ -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) {

src/math/lp/lp_primal_core_solver.h

@@ -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;
                 } 

src/math/lp/lp_primal_core_solver_tableau_def.h

@@ -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);
         }

src/math/lp/static_matrix.h

@@ -2,9 +2,7 @@
 Copyright (c) 2017 Microsoft Corporation
 
 Author:
-
     Lev Nachmanson (levnach)
-
 --*/
 
 #pragma once
@@ -204,7 +202,7 @@ class static_matrix
     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 @@ class static_matrix
             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

src/math/lp/static_matrix_def.h

@@ -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));
     }