mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

deal with compiler warnings

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-08 20:39:19 -08:00
parent 88fbf6510f
commit 857557ad93
8 changed files with 29 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/hnf_cutter.cpp
View file

@ -49,7 +49,7 @@ namespace lp {
m_constraints_for_explanation.push_back(ci);
for (const auto &p : *t) {
for (lar_term::ival p : *t) {
m_var_register.add_var(p.column().index(), true); // hnf only deals with integral variables for now
mpq t = abs(ceil(p.coeff()));
if (t > m_abs_max)

6
src/math/lp/int_solver.cpp
View file

@ -189,7 +189,7 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
}
bool int_solver::cut_indices_are_columns() const {
for (const auto & p: m_t) {
for (lar_term::ival p : m_t) {
if (p.column().index() >= lra.A_r().column_count())
return false;
}
@ -347,7 +347,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
lp_assert(settings().use_tableau());
const auto & A = lra.A_r();
unsigned rounds = 0;
for (const auto &c : A.column(j)) {
for (auto c : A.column(j)) {
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index];
@ -357,7 +357,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
}
TRACE("random_update", tout << "m = " << m << "\n";);
for (const auto &c : A.column(j)) {
for (auto c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break;
row_index = c.var();
const mpq & a = c.coeff();

14
src/math/lp/nla_core.cpp
View file

@ -55,7 +55,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
rational core::value(const lp::lar_term& r) const {
rational ret(0);
for (const auto & t : r) {
for (lp::lar_term::ival t : r) {
ret += t.coeff() * val(t.column());
}
return ret;
@ -63,7 +63,7 @@ rational core::value(const lp::lar_term& r) const {
lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const {
lp::lar_term r;
for (const auto& p : t) {
for (lp::lar_term::ival p : t) {
lpvar j = p.column();
if (lp::tv::is_term(j))
j = m_lar_solver.map_term_index_to_column_index(j);
@ -288,7 +288,7 @@ bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::ex
}
bool core::explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
rational b(0); // the bound
for (const auto& p : t) {
for (lp::lar_term::ival p : t) {
rational pb;
if (explain_coeff_lower_bound(p, pb, e)) {
b += pb;
@ -587,7 +587,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
auto & in = l.ineqs()[i];
print_ineq(in, out);
if (i + 1 < l.ineqs().size()) out << " or ";
for (const auto & p: in.term())
for (lp::lar_term::ival p: in.term())
vars.insert(p.column());
}
out << std::endl;
@ -708,7 +708,7 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &
bool seen_minus = false;
bool seen_plus = false;
i = null_lpvar;
for(const auto & p : t) {
for(lp::lar_term::ival p : t) {
const auto & c = p.coeff();
if (c == 1) {
seen_plus = true;
@ -851,11 +851,11 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
};
for (const auto& i : l.ineqs()) {
for (const auto& p : i.term()) {
for (lp::lar_term::ival p : i.term()) {
insert_j(p.column());
}
}
for (const auto& p : l.expl()) {
for (auto p : l.expl()) {
const auto& c = m_lar_solver.constraints()[p.ci()];
for (const auto& r : c.coeffs()) {
insert_j(r.second);

2
src/math/lp/nra_solver.cpp
View file

@ -204,7 +204,7 @@ struct solver::imp {
// variable representing the term.
svector<polynomial::var> vars;
rational den(1);
for (const auto& kv : t) {
for (lp::lar_term::ival kv : t) {
vars.push_back(lp2nl(kv.column().index()));
den = lcm(den, denominator(kv.coeff()));
}

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

@ -27,7 +27,7 @@ template <typename T, typename X>
template <typename M>
void square_sparse_matrix<T, X>::copy_column_from_input(unsigned input_column, const M& A, unsigned j) {
vector<indexed_value<T>> & new_column_vector = m_columns[j].m_values;
for (const auto & c : A.column(input_column)) {
for (auto c : A.column(input_column)) {
unsigned col_offset = static_cast<unsigned>(new_column_vector.size());
vector<indexed_value<T>> & row_vector = m_rows[c.var()];
unsigned row_offset = static_cast<unsigned>(row_vector.size());
@ -41,7 +41,7 @@ template <typename T, typename X>
template <typename M>
void square_sparse_matrix<T, X>::copy_column_from_input_with_possible_zeros(const M& A, unsigned j) {
vector<indexed_value<T>> & new_column_vector = m_columns[j].m_values;
for (const auto & c : A.column(j)) {
for (auto c : A.column(j)) {
if (is_zero(c.coeff()))
continue;
unsigned col_offset = static_cast<unsigned>(new_column_vector.size());

10
src/sat/smt/arith_solver.cpp
View file

@ -316,7 +316,7 @@ namespace arith {
if (e1->get_sort() != e2->get_sort())
return;
reset_evidence();
for (auto const& ev : e)
for (auto ev : e)
set_evidence(ev.ci(), m_core, m_eqs);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2);
ctx.propagate(n1, n2, jst->to_index());
@ -1035,7 +1035,7 @@ namespace arith {
rational c1(0);
m_nla->am().set(r1, c1.to_mpq());
m_nla->am().add(r, r1, r);
for (auto const& arg : term) {
for (lp::lar_term::ival arg : term) {
auto wi = lp().column2tv(arg.column());
c1 = arg.coeff() * wcoeff;
if (wi.is_term()) {
@ -1108,7 +1108,7 @@ namespace arith {
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
reset_evidence();
for (auto const& ev : m_explanation)
for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs);
// The call mk_bound() can set the m_infeasible_column in lar_solver
// so the explanation is safer to take before this call.
@ -1168,7 +1168,7 @@ namespace arith {
++m_num_conflicts;
++m_stats.m_conflicts;
for (auto const& ev : m_explanation)
for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs);
TRACE("arith",
tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
@ -1305,7 +1305,7 @@ namespace arith {
void solver::term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
TRACE("arith", lp().print_term(term, tout) << "\n";);
for (const auto& ti : term) {
for (lp::lar_term::ival ti : term) {
theory_var w;
auto tv = lp().column2tv(ti.column());
if (tv.is_term()) {

16
src/smt/theory_lra.cpp
View file

@ -1861,7 +1861,7 @@ public:
void dump_cut_lemma(std::ostream& out, lp::lar_term const& term, lp::mpq const& k, lp::explanation const& ex, bool upper) {
lp().print_term(term, out << "bound: ");
out << (upper?" <= ":" >= ") << k << "\n";
for (auto const& p : term) {
for (lp::lar_term::ival p : term) {
auto ti = lp().column2tv(p.column());
out << p.coeff() << " * ";
if (ti.is_term()) {
@ -1871,11 +1871,11 @@ public:
out << "v" << lp().local_to_external(ti.id()) << "\n";
}
}
for (auto const& ev : ex) {
for (auto ev : ex) {
lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
}
expr_ref_vector fmls(m);
for (auto const& ev : ex) {
for (auto ev : ex) {
fmls.push_back(constraint2fml(ev.ci()));
}
expr_ref t(term2expr(term), m);
@ -1936,7 +1936,7 @@ public:
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
reset_evidence();
for (auto const& ev : m_explanation) {
for (auto ev : m_explanation) {
set_evidence(ev.ci(), m_core, m_eqs);
}
// The call mk_bound() can set the m_infeasible_column in lar_solver
@ -2304,7 +2304,7 @@ public:
if (m.is_ite(e1) || m.is_ite(e2))
return;
reset_evidence();
for (auto const& ev : e)
for (auto ev : e)
set_evidence(ev.ci(), m_core, m_eqs);
justification* js = ctx().mk_justification(
ext_theory_eq_propagation_justification(
@ -2709,7 +2709,7 @@ public:
SASSERT(ti.is_term());
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(ti);
for (auto const& p : term) {
for (auto p : term) {
lp::tv wi = lp().column2tv(p.column());
if (wi.is_term()) {
m_todo_vars.push_back(wi);
@ -2735,7 +2735,7 @@ public:
SASSERT(ti.is_term());
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(ti);
for (auto const& coeff : term) {
for (auto coeff : term) {
auto wi = lp().column2tv(coeff.column());
if (wi.is_term()) {
m_todo_vars.push_back(wi);
@ -3174,7 +3174,7 @@ public:
++m_stats.m_conflicts;
TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
for (auto const& ev : m_explanation) {
for (auto ev : m_explanation) {
set_evidence(ev.ci(), m_core, m_eqs);
}
// SASSERT(validate_conflict(m_core, m_eqs));

4
src/util/container_util.h
View file

@ -30,7 +30,7 @@ Revision History:
template<class Set1, class Set2>
void set_intersection(Set1 & tgt, const Set2 & src) {
svector<typename Set1::data> to_remove;
for (typename Set1::data const& itm : tgt)
for (auto itm : tgt)
if (!src.contains(itm))
to_remove.push_back(itm);
while (!to_remove.empty()) {
@ -41,7 +41,7 @@ void set_intersection(Set1 & tgt, const Set2 & src) {
template<class Set>
void set_difference(Set & tgt, const Set & to_remove) {
for (auto const& itm : to_remove)
for (auto itm : to_remove)
tgt.remove(itm);
}