mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
deal with compiler warnings, from MacOS CI build
This commit is contained in:
parent
7eceeff349
commit
f29a596070
13 changed files with 19 additions and 25 deletions
|
@ -221,7 +221,7 @@ class create_cut {
|
|||
for (const auto & p : m_row) {
|
||||
dump_declaration(out, p.var());
|
||||
}
|
||||
for (const auto& p : m_t) {
|
||||
for (lar_term::ival p : m_t) {
|
||||
auto t = lia.lra.column2tv(p.column());
|
||||
if (t.is_term()) {
|
||||
dump_declaration(out, t.id());
|
||||
|
@ -252,7 +252,7 @@ class create_cut {
|
|||
}
|
||||
|
||||
std::ostream& dump_term_coefficients(std::ostream & out) const {
|
||||
for (const auto& p : m_t) {
|
||||
for (lar_term::ival p : m_t) {
|
||||
dump_coeff(out, p);
|
||||
}
|
||||
return out;
|
||||
|
|
|
@ -103,7 +103,7 @@ namespace lp {
|
|||
}
|
||||
usual_delta:
|
||||
mpq delta = zero_of_type<mpq>();
|
||||
for (const auto & p : t)
|
||||
for (lar_term::ival p : t)
|
||||
if (lia.column_is_int(p.column()))
|
||||
delta += abs(p.coeff());
|
||||
|
||||
|
|
|
@ -239,9 +239,8 @@ public:
|
|||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
out << "number of constraints = " << m_constraints.size() << std::endl;
|
||||
for (auto const& c : indices()) {
|
||||
for (constraint_index c : indices())
|
||||
display(out << "(" << c << ") ", *m_constraints[c]);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
@ -337,7 +337,7 @@ namespace lp {
|
|||
auto& jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now
|
||||
lp_assert(jset.empty());
|
||||
|
||||
for (const auto& p : term) {
|
||||
for (lar_term::ival p : term) {
|
||||
unsigned j = p.column();
|
||||
rslv.m_costs[j] = zero_of_type<mpq>();
|
||||
int i = rslv.m_basis_heading[j];
|
||||
|
@ -367,7 +367,7 @@ namespace lp {
|
|||
lp_assert(costs_are_zeros_for_r_solver());
|
||||
lp_assert(reduced_costs_are_zeroes_for_r_solver());
|
||||
rslv.m_costs.resize(A_r().column_count(), zero_of_type<mpq>());
|
||||
for (const auto& p : term) {
|
||||
for (lar_term::ival p : term) {
|
||||
unsigned j = p.column();
|
||||
rslv.m_costs[j] = p.coeff();
|
||||
if (rslv.m_basis_heading[j] < 0)
|
||||
|
@ -1069,7 +1069,7 @@ namespace lp {
|
|||
if (tv::is_term(var)) {
|
||||
lar_term const& t = get_term(var);
|
||||
value = 0;
|
||||
for (auto const& cv : t) {
|
||||
for (lar_term::ival cv : t) {
|
||||
impq const& r = get_column_value(cv.column());
|
||||
if (!numeric_traits<mpq>::is_zero(r.y)) return false;
|
||||
value += r.x * cv.coeff();
|
||||
|
@ -1185,7 +1185,7 @@ namespace lp {
|
|||
return get_value(column_index(term_j));
|
||||
#endif
|
||||
mpq r(0);
|
||||
for (const auto& p : get_term(t))
|
||||
for (lar_term::ival p : get_term(t))
|
||||
r += p.coeff() * get_value(p.column());
|
||||
return r;
|
||||
}
|
||||
|
@ -1194,7 +1194,7 @@ namespace lp {
|
|||
if (t.is_var())
|
||||
return get_column_value(t.column());
|
||||
impq r;
|
||||
for (const auto& p : get_term(t))
|
||||
for (lar_term::ival p : get_term(t))
|
||||
r += p.coeff() * get_column_value(p.column());
|
||||
return r;
|
||||
}
|
||||
|
@ -1744,7 +1744,7 @@ namespace lp {
|
|||
m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1));
|
||||
if (use_lu())
|
||||
fill_last_row_of_A_d(A_d(), term);
|
||||
for (const auto& c : *term) {
|
||||
for (lar_term::ival c : *term) {
|
||||
unsigned j = c.column();
|
||||
while (m_usage_in_terms.size() <= j) {
|
||||
m_usage_in_terms.push_back(0);
|
||||
|
@ -2326,7 +2326,7 @@ namespace lp {
|
|||
continue;
|
||||
bool need_to_fix = false;
|
||||
const lar_term& t = *m_terms[i];
|
||||
for (const auto& p : t) {
|
||||
for (lar_term::ival p : t) {
|
||||
if (m_incorrect_columns.contains(p.column())) {
|
||||
need_to_fix = true;
|
||||
break;
|
||||
|
@ -2343,7 +2343,7 @@ namespace lp {
|
|||
// return true if all y coords are zeroes
|
||||
bool lar_solver::sum_first_coords(const lar_term& t, mpq& val) const {
|
||||
val = zero_of_type<mpq>();
|
||||
for (const auto& c : t) {
|
||||
for (lar_term::ival c : t) {
|
||||
const auto& x = m_mpq_lar_core_solver.m_r_x[c.column()];
|
||||
if (!is_zero(x.y))
|
||||
return false;
|
||||
|
|
|
@ -466,7 +466,7 @@ public:
|
|||
return false;
|
||||
TRACE("nla_solver", tout << "j" << j << " not blocked\n";);
|
||||
impq delta = get_column_value(j) - ival;
|
||||
for (const auto &c : A_r().column(j)) {
|
||||
for (auto c : A_r().column(j)) {
|
||||
unsigned row_index = c.var();
|
||||
const mpq & a = c.coeff();
|
||||
unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];
|
||||
|
|
|
@ -158,13 +158,13 @@ public:
|
|||
bool is_normalized() const {
|
||||
lpvar min_var = -1;
|
||||
mpq c;
|
||||
for (const auto & p : *this) {
|
||||
for (ival p : *this) {
|
||||
if (p.column() < min_var) {
|
||||
min_var = p.column();
|
||||
}
|
||||
}
|
||||
lar_term r;
|
||||
for (const auto & p : *this) {
|
||||
for (ival p : *this) {
|
||||
if (p.column() == min_var) {
|
||||
return p.coeff().is_one();
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue