mirror of
https://github.com/Z3Prover/z3
synced 2025-08-11 13:40:52 +00:00
Replace static_cast with usize utility function
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
1c680f32c1
commit
c1c89cc047
5 changed files with 23 additions and 18 deletions
|
@ -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<unsigned>(clauses.size()));
|
||||
literal_special_kind.resize(static_cast<unsigned>(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<unsigned> vec_id;
|
||||
for (unsigned i = 0, sz = static_cast<unsigned>(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<unsigned>(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<unsigned>(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)) {
|
||||
|
|
|
@ -33,7 +33,7 @@ namespace nlsat {
|
|||
m_learned.clear();
|
||||
|
||||
IF_VERBOSE(3, s.display(verbose_stream() << "before\n"));
|
||||
unsigned sz = static_cast<unsigned>(m_clauses.size());
|
||||
unsigned sz = usize(m_clauses);
|
||||
while (true) {
|
||||
|
||||
subsumption_simplify();
|
||||
|
@ -51,7 +51,7 @@ namespace nlsat {
|
|||
|
||||
split_factors();
|
||||
|
||||
sz = static_cast<unsigned>(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<poly> ps;
|
||||
buffer<bool> is_even;
|
||||
unsigned num_atoms = static_cast<unsigned>(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<literal> const& b2l) {
|
||||
literal_vector lits;
|
||||
unsigned n = static_cast<unsigned>(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<unsigned>(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())
|
||||
|
|
|
@ -2603,7 +2603,7 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
bool check_satisfied(clause_vector const & cs) {
|
||||
unsigned sz = static_cast<unsigned>(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<unsigned>(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<unsigned>(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<unsigned>(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<unsigned>(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<unsigned>(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<unsigned>(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";
|
||||
|
|
|
@ -131,7 +131,7 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void collect(clause_vector const & cs) {
|
||||
unsigned sz = static_cast<unsigned>(cs.size());
|
||||
unsigned sz = usize(cs);
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
collect(*(cs[i]));
|
||||
}
|
||||
|
|
|
@ -1249,3 +1249,8 @@ inline std::ostream& operator<<(std::ostream& out, vector<T> const& v) {
|
|||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
template<typename Vec>
|
||||
inline unsigned usize(Vec const& v) {
|
||||
return static_cast<unsigned>(v.size());
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue