From c1c89cc04721a6fe19054f0f08869e3291491b7f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 30 Jun 2025 16:26:26 +0000 Subject: [PATCH] Replace static_cast with usize utility function Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/nlsat/nlsat_simple_checker.cpp | 10 +++++----- src/nlsat/nlsat_simplify.cpp | 10 +++++----- src/nlsat/nlsat_solver.cpp | 14 +++++++------- src/nlsat/nlsat_variable_ordering_strategy.cpp | 2 +- src/util/vector.h | 5 +++++ 5 files changed, 23 insertions(+), 18 deletions(-) diff --git a/src/nlsat/nlsat_simple_checker.cpp b/src/nlsat/nlsat_simple_checker.cpp index c44057234..d98e8b052 100644 --- a/src/nlsat/nlsat_simple_checker.cpp +++ b/src/nlsat/nlsat_simple_checker.cpp @@ -257,8 +257,8 @@ namespace nlsat { for (unsigned i = 0; i < arith_var_num; ++i) { vars_domain.push_back(Var_Domain(am)); } - clauses_visited.resize(static_cast(clauses.size())); - literal_special_kind.resize(static_cast(clauses.size())); + clauses_visited.resize(usize(clauses)); + literal_special_kind.resize(usize(clauses)); } sign_kind to_sign_kind(atom::kind kd) { if (kd == atom::EQ) @@ -1067,7 +1067,7 @@ else { // ( == 0) + (c > 0) -> > 0 bool collect_var_domain() { // vector vec_id; - for (unsigned i = 0, sz = static_cast(clauses.size()); i < sz; ++i) { + for (unsigned i = 0, sz = usize(clauses); i < sz; ++i) { if (clauses_visited[i].visited) continue; if (clauses[i]->size() > 1) @@ -1099,7 +1099,7 @@ else { // ( == 0) + (c > 0) -> > 0 tout << "====== arith[" << i << "] ======\n"; } ); - for (unsigned i = 0, sz = static_cast(clauses.size()); i < sz; ++i) { + for (unsigned i = 0, sz = usize(clauses); i < sz; ++i) { // unsigned id = vec_id[i]; if (!collect_domain_axbsc_form(i, 0)) return false; @@ -1520,7 +1520,7 @@ else { // ( == 0) + (c > 0) -> > 0 return false; } bool check() { - for (unsigned i = 0, sz = static_cast(clauses.size()); i < sz; ++i) { + for (unsigned i = 0, sz = usize(clauses); i < sz; ++i) { if (clauses_visited[i].visited) continue; if (!check_clause_satisfiable(i)) { diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp index fdc7f984c..f4ff51bff 100644 --- a/src/nlsat/nlsat_simplify.cpp +++ b/src/nlsat/nlsat_simplify.cpp @@ -33,7 +33,7 @@ namespace nlsat { m_learned.clear(); IF_VERBOSE(3, s.display(verbose_stream() << "before\n")); - unsigned sz = static_cast(m_clauses.size()); + unsigned sz = usize(m_clauses); while (true) { subsumption_simplify(); @@ -51,7 +51,7 @@ namespace nlsat { split_factors(); - sz = static_cast(m_clauses.size()); + sz = usize(m_clauses); } IF_VERBOSE(3, s.display(verbose_stream() << "after\n")); @@ -66,7 +66,7 @@ namespace nlsat { polynomial_ref p(m_pm); ptr_buffer ps; buffer is_even; - unsigned num_atoms = static_cast(m_atoms.size()); + unsigned num_atoms = usize(m_atoms); for (unsigned j = 0; j < num_atoms; ++j) { atom* a1 = m_atoms[j]; if (a1 && a1->is_ineq_atom()) { @@ -94,7 +94,7 @@ namespace nlsat { void update_clauses(u_map const& b2l) { literal_vector lits; - unsigned n = static_cast(m_clauses.size()); + unsigned n = usize(m_clauses); for (unsigned i = 0; i < n; ++i) { clause* c = m_clauses[i]; @@ -334,7 +334,7 @@ namespace nlsat { } bool cleanup_removed() { - unsigned j = 0, sz = static_cast(m_clauses.size()); + unsigned j = 0, sz = usize(m_clauses); for (unsigned i = 0; i < sz; ++i) { auto c = m_clauses[i]; if (c->is_removed()) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 323b7dadc..eb082afd7 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2603,7 +2603,7 @@ namespace nlsat { } bool check_satisfied(clause_vector const & cs) { - unsigned sz = static_cast(cs.size()); + unsigned sz = usize(cs); for (unsigned i = 0; i < sz; i++) { clause const & c = *(cs[i]); if (!is_satisfied(c)) { @@ -2616,7 +2616,7 @@ namespace nlsat { bool check_satisfied() { TRACE(nlsat, tout << "bk: b" << m_bk << ", xk: x" << m_xk << "\n"; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << "\n"; }); - unsigned num = static_cast(m_atoms.size()); + unsigned num = usize(m_atoms); if (m_bk != null_bool_var) num = m_bk; for (bool_var b = 0; b < num; b++) { @@ -2713,7 +2713,7 @@ namespace nlsat { } void collect(clause_vector const & cs) { - unsigned sz = static_cast(cs.size()); + unsigned sz = usize(cs); for (unsigned i = 0; i < sz; i++) collect(*(cs[i])); } @@ -3045,7 +3045,7 @@ namespace nlsat { unsigned num = num_vars(); for (unsigned i = 0; i < num; i++) { clause_vector & ws = m_watches[i]; - sort_clauses_by_degree(static_cast(ws.size()), ws.data()); + sort_clauses_by_degree(usize(ws), ws.data()); } } @@ -3273,7 +3273,7 @@ namespace nlsat { } std::ostream& display_bool_assignment(std::ostream & out, bool eval_atoms = false) const { - unsigned sz = static_cast(m_atoms.size()); + unsigned sz = usize(m_atoms); if (!eval_atoms) { for (bool_var b = 0; b < sz; b++) { if (m_bvalues[b] == l_undef) @@ -3945,7 +3945,7 @@ namespace nlsat { } std::ostream& display_mathematica(std::ostream & out, clause_vector const & cs) const { - unsigned sz = static_cast(cs.size()); + unsigned sz = usize(cs); for (unsigned i = 0; i < sz; i++) { if (i > 0) out << ",\n"; display_mathematica(out << " ", *(cs[i])); @@ -4011,7 +4011,7 @@ namespace nlsat { } std::ostream& display_smt2_bool_decls(std::ostream & out) const { - unsigned sz = static_cast(m_atoms.size()); + unsigned sz = usize(m_atoms); for (unsigned i = 0; i < sz; i++) { if (m_atoms[i] == nullptr) out << "(declare-fun b" << i << " () Bool)\n"; diff --git a/src/nlsat/nlsat_variable_ordering_strategy.cpp b/src/nlsat/nlsat_variable_ordering_strategy.cpp index e668cd654..61007c212 100644 --- a/src/nlsat/nlsat_variable_ordering_strategy.cpp +++ b/src/nlsat/nlsat_variable_ordering_strategy.cpp @@ -131,7 +131,7 @@ namespace nlsat { } void collect(clause_vector const & cs) { - unsigned sz = static_cast(cs.size()); + unsigned sz = usize(cs); for (unsigned i = 0; i < sz; i++) collect(*(cs[i])); } diff --git a/src/util/vector.h b/src/util/vector.h index 67f6218ed..bb3aa18b4 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -1249,3 +1249,8 @@ inline std::ostream& operator<<(std::ostream& out, vector const& v) { } return out; } + +template +inline unsigned usize(Vec const& v) { + return static_cast(v.size()); +}