mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

using C++11 features to simplify for-loops

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-23 07:56:28 +07:00
parent 5c5673bc09
commit cd0d52acec
1 changed files with 4 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/macros/macro_util.cpp
View file

@ -417,13 +417,11 @@ bool macro_util::is_quasi_macro_ok(expr * n, unsigned num_decls, expr * def) con
if (is_app(n) && if (is_app(n) &&
to_app(n)->get_family_id() == null_family_id && to_app(n)->get_family_id() == null_family_id &&
to_app(n)->get_num_args() >= num_decls) { to_app(n)->get_num_args() >= num_decls) {
unsigned num_args = to_app(n)->get_num_args();
sbuffer<bool> found_vars; sbuffer<bool> found_vars;
found_vars.resize(num_decls, false); found_vars.resize(num_decls, false);
unsigned num_found_vars = 0; unsigned num_found_vars = 0;
expr_free_vars fv; expr_free_vars fv;
for (unsigned i = 0; i < num_args; i++) { for (expr* arg : *to_app(n)) {
expr * arg = to_app(n)->get_arg(i);
if (occurs(to_app(n)->get_decl(), arg)) if (occurs(to_app(n)->get_decl(), arg))
return false; return false;
else else
@ -553,12 +551,9 @@ bool is_hint_head(expr * n, ptr_buffer<var> & vars) {
return false; return false;
if (to_app(n)->get_decl()->is_associative() || to_app(n)->get_family_id() != null_family_id) if (to_app(n)->get_decl()->is_associative() || to_app(n)->get_family_id() != null_family_id)
return false; return false;
unsigned num_args = to_app(n)->get_num_args(); for (expr * arg : *to_app(n))
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(n)->get_arg(i);
if (is_var(arg)) if (is_var(arg))
vars.push_back(to_var(arg)); vars.push_back(to_var(arg));
}
return !vars.empty(); return !vars.empty();
} }
@ -579,9 +574,7 @@ bool vars_of_is_subset(expr * n, ptr_buffer<var> const & vars) {
return false; return false;
} }
else if (is_app(curr)) { else if (is_app(curr)) {
unsigned num_args = to_app(curr)->get_num_args(); for (expr * arg : *to_app(curr)) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(curr)->get_arg(i);
if (is_ground(arg)) if (is_ground(arg))
continue; continue;
if (visited.contains(arg)) if (visited.contains(arg))
@ -611,13 +604,11 @@ bool is_hint_atom(expr * lhs, expr * rhs) {
} }
void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_ref & new_head) { void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_ref & new_head) {
unsigned num_args = head->get_num_args();
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
sbuffer<bool> found_vars; sbuffer<bool> found_vars;
found_vars.resize(num_decls, false); found_vars.resize(num_decls, false);
unsigned next_var_idx = num_decls; unsigned next_var_idx = num_decls;
for (unsigned i = 0; i < num_args; i++) { for (expr * arg : *head) {
expr * arg = head->get_arg(i);
if (is_var(arg)) { if (is_var(arg)) {
unsigned idx = to_var(arg)->get_idx(); unsigned idx = to_var(arg)->get_idx();
SASSERT(idx < num_decls); SASSERT(idx < num_decls);