mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge pull request #1972 from waywardmonkeys/use-vector-empty

Browse source 
Prefer using empty rather than size comparisons.
This commit is contained in:
Nikolaj Bjorner 2018-11-27 10:39:34 -08:00 • committed by GitHub
commit 5df29daa35
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
56 changed files with 104 additions and 104 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/proto_model/array_factory.cpp
View file

@ -104,7 +104,7 @@ bool array_factory::mk_two_diff_values_for(sort * s) {
bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
value_set * set = nullptr;
if (!m_sort2value_set.find(s, set) || set->size() == 0) {
if (!m_sort2value_set.find(s, set) || set->empty()) {
if (!mk_two_diff_values_for(s))
return false;
}

2
src/smt/smt_case_split_queue.cpp
View file

@ -281,7 +281,7 @@ namespace smt {
}
}
if (order == 1) {
if (undef_children.size() == 0) {
if (undef_children.empty()) {
// a bug?
} else if (undef_children.size() == 1) {
undef_child = undef_children[0];

4
src/smt/theory_arith_aux.h
View file

@ -548,7 +548,7 @@ namespace smt {
if (!it->is_dead()) {
row const & r = m_rows[it->m_row_id];
theory_var s = r.get_base_var();
if (is_quasi_base(s) && m_var_occs[s].size() == 0)
if (is_quasi_base(s) && m_var_occs[s].empty())
continue;
if (is_int(v)) {
numeral const & c = r[it->m_row_idx].m_coeff;
@ -574,7 +574,7 @@ namespace smt {
TRACE("move_unconstrained_to_base", tout << "before...\n"; display(tout););
int num = get_num_vars();
for (theory_var v = 0; v < num; v++) {
if (m_var_occs[v].size() == 0 && is_free(v)) {
if (m_var_occs[v].empty() && is_free(v)) {
switch (get_var_kind(v)) {
case QUASI_BASE:
break;

2
src/smt/theory_array_full.cpp
View file

@ -141,7 +141,7 @@ namespace smt {
}
void theory_array_full::set_prop_upward(theory_var v, var_data* d) {
if (m_params.m_array_always_prop_upward || d->m_stores.size() >= 1) {
if (m_params.m_array_always_prop_upward || !d->m_stores.empty()) {
theory_array::set_prop_upward(v, d);
}
else {

2
src/smt/theory_recfun.h
View file

@ -125,7 +125,7 @@ namespace smt {
literal mk_eq_lit(expr* l, expr* r);
bool is_standard_order(recfun::vars const& vars) const {
return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0;
return vars.empty() || vars[vars.size()-1]->get_idx() == 0;
}
protected:
void push_case_expand(case_expansion* e) { m_q_case_expand.push_back(e); }

10
src/smt/theory_seq.cpp
View file

@ -3576,18 +3576,18 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
}
void theory_seq::display(std::ostream & out) const {
if (m_eqs.size() == 0 &&
m_nqs.size() == 0 &&
if (m_eqs.empty() &&
m_nqs.empty() &&
m_rep.empty() &&
m_exclude.empty()) {
return;
}
out << "Theory seq\n";
if (m_eqs.size() > 0) {
if (!m_eqs.empty()) {
out << "Equations:\n";
display_equations(out);
}
if (m_nqs.size() > 0) {
if (!m_nqs.empty()) {
display_disequations(out);
}
if (!m_re2aut.empty()) {
@ -3661,7 +3661,7 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co
for (literal lit : e.lits()) {
out << lit << " ";
}
if (e.lits().size() > 0) {
if (!e.lits().empty()) {
out << "\n";
}
for (unsigned j = 0; j < e.ls().size(); ++j) {

24
src/smt/theory_str.cpp
View file

@ -2501,7 +2501,7 @@ namespace smt {
}
}
if (resolvedMap.size() == 0) {
if (resolvedMap.empty()) {
// no simplification possible
return node;
} else {
@ -5452,7 +5452,7 @@ namespace smt {
}
if (implyR) {
if (litems1.size() == 0) {
if (litems1.empty()) {
assert_axiom(implyR);
} else {
assert_implication(mk_and(litems1), implyR);
@ -7020,7 +7020,7 @@ namespace smt {
bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) {
ENSURE(aut != nullptr);
if (aut->final_states().size() < 1) {
if (aut->final_states().empty()) {
// no solutions at all
refined_lower_bound = rational::minus_one();
return false;
@ -8168,13 +8168,13 @@ namespace smt {
// step 2: Concat == Constant
if (eqc_const_lhs.size() != 0) {
if (!eqc_const_lhs.empty()) {
expr * conStr = *(eqc_const_lhs.begin());
std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
for (; itor2 != eqc_concat_rhs.end(); itor2++) {
solve_concat_eq_str(*itor2, conStr);
}
} else if (eqc_const_rhs.size() != 0) {
} else if (!eqc_const_rhs.empty()) {
expr* conStr = *(eqc_const_rhs.begin());
std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
for (; itor1 != eqc_concat_lhs.end(); itor1++) {
@ -8250,7 +8250,7 @@ namespace smt {
ast_manager & m = get_manager();
int hasCommon = 0;
if (eqc_concat_lhs.size() != 0 && eqc_concat_rhs.size() != 0) {
if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) {
std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
for (; itor1 != eqc_concat_lhs.end(); itor1++) {
@ -8570,13 +8570,13 @@ namespace smt {
obj_map<expr, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
while (varItor != cut_var_map.end()) {
std::stack<T_cut*> & val = cut_var_map[varItor->m_key];
while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
while ((!val.empty()) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
// TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout););
// T_cut * aCut = val.top();
val.pop();
// dealloc(aCut);
}
if (val.size() == 0) {
if (val.empty()) {
cutvarmap_removes.insert(varItor->m_key);
}
varItor++;
@ -9402,7 +9402,7 @@ namespace smt {
}
}
if (depMap.size() == 0) {
if (depMap.empty()) {
std::map<expr*, int>::iterator itor = strVarMap.begin();
for (; itor != strVarMap.end(); itor++) {
expr * var = get_alias_index_ast(aliasIndexMap, itor->first);
@ -10801,7 +10801,7 @@ namespace smt {
expr * var = fvIt2->first;
tmpSet.clear();
get_eqc_allUnroll(var, constValue, tmpSet);
if (tmpSet.size() > 0) {
if (!tmpSet.empty()) {
fv_unrolls_map[var] = tmpSet;
}
}
@ -10935,7 +10935,7 @@ namespace smt {
expr * var = fvIt1->first;
fSimpUnroll.clear();
get_eqc_simpleUnroll(var, constValue, fSimpUnroll);
if (fSimpUnroll.size() == 0) {
if (fSimpUnroll.empty()) {
gen_assign_unroll_reg(fv_unrolls_map[var]);
} else {
expr * toAssert = gen_assign_unroll_Str2Reg(var, fSimpUnroll);
@ -11548,7 +11548,7 @@ namespace smt {
unroll_tries_map[var][unrolls].erase(e);
}
if (unroll_tries_map[var][unrolls].size() == 0) {
if (unroll_tries_map[var][unrolls].empty()) {
unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var());
}

2
src/smt/theory_utvpi_def.h
View file

@ -618,7 +618,7 @@ namespace smt {
th_var v1 = null_theory_var, v2 = null_theory_var;
bool pos1 = true, pos2 = true;
if (terms.size() >= 1) {
if (!terms.empty()) {
v1 = terms[0].first;
pos1 = terms[0].second.is_one();
SASSERT(v1 != null_theory_var);