From 4ca6d6951fcdc9af2d91bacbb8dd481bd17c59a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2021 17:31:27 -0800 Subject: [PATCH] use updated C++ features --- src/qe/mbp/mbp_datatypes.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/qe/mbp/mbp_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp index 7c5d43afb7c..a3230f5414b 100644 --- a/src/qe/mbp/mbp_datatypes.cpp +++ b/src/qe/mbp/mbp_datatypes.cpp @@ -196,16 +196,16 @@ namespace mbp { expr_mark visited; expr_mark has_var; bool inserted = false; - for (unsigned i = 0; i < vars.size(); ++i) { - if (m.is_bool(vars[i])) continue; - if (dt.is_datatype(m.get_sort(vars[i]))) continue; + for (app* v : vars) { + if (m.is_bool(v)) continue; + if (dt.is_datatype(m.get_sort(v))) continue; inserted = true; - has_var.mark(vars[i]); - visited.mark(vars[i]); + has_var.mark(v); + visited.mark(v); } if (inserted) { for (unsigned i = 0; i < lits.size(); ++i) { - expr* e = lits[i].get(), *l, *r; + expr* e = lits.get(i), *l, *r; if (m.is_eq(e, l, r) && reduce_eq(visited, has_var, l, r, lits)) { project_plugin::erase(lits, i); reduced = true; @@ -258,8 +258,7 @@ namespace mbp { } app* f = to_app(_f); bool has_new = false, has_v = false; - for (unsigned i = 0; i < f->get_num_args(); ++i) { - expr* arg = f->get_arg(i); + for (expr* arg : *f) { if (!visited.is_marked(arg)) { todo.push_back(arg); has_new = true;