mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

refactoring to use for-range

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-15 10:57:31 -07:00
parent 7ebe7c46b9
commit 47c12f9a18
7 changed files with 20 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/ddnf/ddnf.cpp
View file

@ -652,8 +652,8 @@ namespace datalog {
void init_ctx(rule_set& rules) {
m_inner_ctx.reset();
func_decl_set const& predicates = m_ctx.get_predicates();
for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) {
m_inner_ctx.register_predicate(*fit, false);
for (auto* fit : predicates) {
m_inner_ctx.register_predicate(fit, false);
}
m_inner_ctx.ensure_opened();
m_inner_ctx.replace_rules(rules);

10
src/smt/smt_context.cpp
View file

@ -3185,15 +3185,13 @@ namespace smt {
TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
// now find the sets of literals which contain l
vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
literal_vector case_split_set = *it;
for (const auto& case_split_set : case_split_sets) {
TRACE("theory_case_split", tout << "found case split set { ";
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
tout << set_it->index() << " ";
for (const auto& set_elem : case_split_set) {
tout << set_elem.index() << " ";
}
tout << "}" << std::endl;);
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
literal l2 = *set_it;
for (const auto& l2 : case_split_set) {
if (l2 != l) {
b_justification js(l);
TRACE("theory_case_split", tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;);

2
src/tactic/core/cofactor_term_ite_tactic.cpp
View file

@ -30,7 +30,7 @@ class cofactor_term_ite_tactic : public tactic {
void process(goal & g) {
ast_manager & m = g.m();
unsigned idx = 0;
for (auto [f, dep, pr] : g) {
for (const auto& [f, dep, pr] : g) {
if (g.inconsistent())
break;
expr_ref new_f(m);

2
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -853,7 +853,7 @@ class tseitin_cnf_tactic : public tactic {
m_mc = nullptr;
unsigned idx = 0;
for (auto [f, dep, pr] : *g) {
for (const auto& [f, dep, pr] : *g) {
process(f, dep);
g->update(idx++, m.mk_true(), nullptr, nullptr);
}

2
src/tactic/goal.cpp
View file

@ -488,7 +488,7 @@ void goal::shrink(unsigned j) {
*/
void goal::elim_true() {
unsigned i = 0, j = 0;
for (auto [f, dep, pr] : *this) {
for (const auto& [f, dep, pr] : *this) {
if (m().is_true(f)) {
++i;
continue;

12
src/test/algebraic.cpp
View file

@ -25,18 +25,18 @@ Notes:
static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
out << "numbers in decimal:\n";
algebraic_numbers::manager & m = rs.m();
for (unsigned i = 0; i < rs.size(); i++) {
m.display_decimal(out, rs[i], 10);
for (const auto& r : rs) {
m.display_decimal(out, r, 10);
out << "\n";
}
out << "numbers as root objects\n";
for (unsigned i = 0; i < rs.size(); i++) {
m.display_root(out, rs[i]);
for (const auto& r : rs) {
m.display_root(out, r);
out << "\n";
}
out << "numbers as intervals\n";
for (unsigned i = 0; i < rs.size(); i++) {
m.display_interval(out, rs[i]);
for (const auto& r : rs) {
m.display_interval(out, r);
out << "\n";
}
}

14
src/test/hashtable.cpp
View file

@ -83,18 +83,14 @@ static void tst2() {
}
}
{
safe_int_set::iterator it = h2.begin();
safe_int_set::iterator end = h2.end();
for(; it != end; ++it) {
ENSURE(contains(h1, *it));
for (const auto& elem : h2) {
ENSURE(contains(h1, elem));
}
}
{
int_set::iterator it = h1.begin();
int_set::iterator end = h1.end();
int n = 0;
for (; it != end; ++it) {
ENSURE(contains(h1, *it));
for (const auto& elem : h1) {
ENSURE(contains(h1, elem));
n++;
}
ENSURE(n == h1.size());
@ -202,7 +198,7 @@ void test_hashtable_iterators() {
ht.insert(3);
int count = 0;
for(auto it = ht.begin(); it != ht.end(); ++it) {
for (const auto& elem : ht) {
++count;
}
VERIFY(count == 3);