From d025b34606a53df02f195e6f820d2f972ca256dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2026 13:00:35 -0700 Subject: [PATCH] prepare for enodes over lambdas --- src/smt/smt_conflict_resolution.cpp | 2 +- src/smt/smt_context.cpp | 4 ++-- src/smt/smt_context.h | 2 +- src/smt/smt_enode.h | 12 ++++++------ src/smt/smt_internalizer.cpp | 8 ++++---- src/smt/smt_model_finder.cpp | 16 ++++++++-------- src/smt/smt_theory.cpp | 2 +- src/smt/smt_theory.h | 4 ++-- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_array_base.h | 4 ++-- src/smt/theory_array_full.cpp | 6 +++--- src/smt/theory_bv.cpp | 8 ++++++-- src/smt/theory_bv.h | 6 +++--- src/smt/theory_datatype.cpp | 28 ++++++++++++++-------------- src/smt/theory_diff_logic_def.h | 7 +++---- src/smt/theory_dl.cpp | 11 ++++++----- src/smt/theory_pb.cpp | 5 ++--- 17 files changed, 65 insertions(+), 62 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index bf7c62a32..6cb22e505 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -855,7 +855,7 @@ namespace smt { case eq_justification::CONGRUENCE: num_args = n1->get_num_args(); SASSERT(num_args == n2->get_num_args()); - SASSERT(n1->get_app()->get_decl() == n2->get_app()->get_decl()); + SASSERT(n1->get_decl() == n2->get_decl()); if (js.used_commutativity()) { bool visited = true; SASSERT(num_args == 2); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d55b2d98d..61a0d3984 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4672,8 +4672,8 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - auto p = parent->get_app(); - family_id fid = p->get_family_id(); + auto p = parent->get_expr(); + family_id fid = parent->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) continue; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 52e6c5b26..6a77dd435 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1025,7 +1025,7 @@ namespace smt { bool_var mk_bool_var(expr * n); - enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled); + enode * mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled); void attach_th_var(enode * n, theory * th, theory_var v); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index c3122185c..f372081bb 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -59,7 +59,7 @@ namespace smt { equality propagation, and the theory central bus of equalities. */ class enode { - app * m_owner; //!< The application that 'owns' this enode. + expr * m_owner; //!< The application that 'owns' this enode. enode * m_root; //!< Representative of the equivalence class enode * m_next; //!< Next element in the equivalence class. enode * m_cg; @@ -166,7 +166,7 @@ namespace smt { void del_eh(ast_manager & m, bool update_children_parent = true); - app * get_app() const { return m_owner; } + app * get_app() const { SASSERT(is_app()); return to_app(m_owner); } expr *get_expr() const { return m_owner; @@ -179,13 +179,13 @@ namespace smt { unsigned get_owner_id() const { return m_owner->get_id(); } unsigned get_expr_id() const { return m_owner->get_id(); } - func_decl * get_decl() const { return m_owner->get_decl(); } - unsigned get_decl_id() const { return m_owner->get_decl()->get_small_id(); } + func_decl * get_decl() const { return is_app() ? to_app(m_owner)->get_decl() : nullptr; } + unsigned get_decl_id() const { return is_app() ? to_app(m_owner)->get_decl()->get_small_id() : 43; } sort* get_sort() const { return m_owner->get_sort(); } family_id get_family_id() const { - return m_owner->get_family_id(); + return is_app() ? to_app(m_owner)->get_family_id() : basic_family_id; } unsigned hash() const { @@ -225,7 +225,7 @@ namespace smt { } unsigned get_num_args() const { - return m_suppress_args ? 0 : m_owner->get_num_args(); + return m_suppress_args || !is_app() ? 0 : to_app(m_owner)->get_num_args(); } enode * get_arg(unsigned idx) const { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 946a480be..ca7895b69 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -996,7 +996,7 @@ namespace smt { \remark If suppress_args is true, then the enode is viewed as a constant in the egraph. */ - enode * context::mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled) { + enode * context::mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled) { TRACE(mk_enode_detail, tout << mk_pp(n, m) << "\nsuppress_args: " << suppress_args << ", merge_tf: " << merge_tf << ", cgc_enabled: " << cgc_enabled << "\n";); SASSERT(!e_internalized(n)); @@ -1008,7 +1008,7 @@ namespace smt { CTRACE(cached_generation, generation != m_generation, tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";); } - enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, + enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";); if (m.is_unique_value(n)) @@ -1042,7 +1042,7 @@ namespace smt { } } if (!e->is_eq()) { - unsigned decl_id = n->get_decl()->get_small_id(); + unsigned decl_id = e->get_decl_id(); if (decl_id >= m_decl2enodes.size()) m_decl2enodes.resize(decl_id+1); m_decl2enodes[decl_id].push_back(e); @@ -1086,7 +1086,7 @@ namespace smt { m_cg_table.erase(e); } if (e->get_num_args() > 0 && !e->is_eq()) { - unsigned decl_id = to_app(n)->get_decl()->get_small_id(); + unsigned decl_id = e->get_decl_id(); SASSERT(decl_id < m_decl2enodes.size()); SASSERT(m_decl2enodes[decl_id].back() == e); m_decl2enodes[decl_id].pop_back(); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 7506e85af..41c21cc1e 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1378,7 +1378,7 @@ namespace smt { Store in arrays, all enodes that match the pattern */ - void get_auf_arrays(app* auf_arr, context* ctx, ptr_buffer& arrays) { + void get_auf_arrays(expr* auf_arr, context* ctx, ptr_buffer& arrays) { if (is_ground(auf_arr)) { if (ctx->e_internalized(auf_arr)) { enode* e = ctx->get_enode(auf_arr); @@ -1387,8 +1387,8 @@ namespace smt { } } } - else { - app* nested_array = to_app(auf_arr->get_arg(0)); + else if (is_app(auf_arr)) { + app* nested_array = to_app(to_app(auf_arr)->get_arg(0)); ptr_buffer nested_arrays; get_auf_arrays(nested_array, ctx, nested_arrays); for (enode* curr : nested_arrays) { @@ -1396,7 +1396,7 @@ namespace smt { enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { enode* p = *it2; - if (ctx->is_relevant(p) && p->get_decl() == auf_arr->get_decl()) { + if (ctx->is_relevant(p) && p->get_decl() == to_app(auf_arr)->get_decl()) { arrays.push_back(p); } } @@ -1411,9 +1411,9 @@ namespace smt { unsigned m_arg_i; unsigned m_var_j; - app* get_array() const { return to_app(m_select->get_arg(0)); } + expr* get_array() const { return m_select->get_arg(0); } - func_decl* get_array_func_decl(app* ground_array, auf_solver& s) { + func_decl* get_array_func_decl(expr* ground_array, auf_solver& s) { TRACE(model_evaluator, tout << expr_ref(ground_array, m) << "\n";); expr* ground_array_interp = s.eval(ground_array, false); if (ground_array_interp && m_array.is_as_array(ground_array_interp)) @@ -1449,7 +1449,7 @@ namespace smt { }); node* n1 = s.get_uvar(q, m_var_j); for (enode* n : arrays) { - auto ground_array = n->get_app(); + auto ground_array = n->get_expr(); func_decl* f = get_array_func_decl(ground_array, s); if (f) { SASSERT(m_arg_i >= 1); @@ -1463,7 +1463,7 @@ namespace smt { ptr_buffer arrays; get_auf_arrays(get_array(), ctx, arrays); for (enode* curr : arrays) { - auto ground_array = curr->get_app(); + auto ground_array = curr->get_expr(); func_decl* f = get_array_func_decl(ground_array, s); if (f) { node* A_f_i = s.get_A_f_i(f, m_arg_i - 1); diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 4b3a53baf..be32edacb 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -204,7 +204,7 @@ namespace smt { log_axiom_instantiation(mk_or(fmls)); } - void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector> & used_enodes) { + void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, expr * const * bindings, unsigned pattern_id, const vector> & used_enodes) { ast_manager & m = get_manager(); SASSERT(r->get_ref_count() > 0); std::ostream& out = m.trace_stream(); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 99da9a0b6..70b5556d6 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -482,11 +482,11 @@ namespace smt { protected: void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, - app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()); void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, - app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 0849639d5..c8fd25dba 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2179,7 +2179,7 @@ namespace smt { TRACE(shared, tout << ctx.get_scope_level() << " " << v << " " << r->get_num_parents() << "\n";); for (; it != end; ++it) { enode * parent = *it; - app * o = parent->get_app(); + app* o = parent->get_app(); if (parent->get_family_id() == get_id()) { switch (o->get_decl_kind()) { case OP_DIV: diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 87d12c156..ea716b49d 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -33,8 +33,8 @@ namespace smt { void add_weak_var(theory_var v); virtual void set_prop_upward(theory_var v) {} void found_unsupported_op(expr * n); - void found_unsupported_op(enode* n) { found_unsupported_op(n->get_app()); } - void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_app()); } + void found_unsupported_op(enode* n) { found_unsupported_op(n->get_expr()); } + void found_unsupported_op(theory_var v) { found_unsupported_op(get_expr(v)); } bool is_store(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_STORE); } bool is_map(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_MAP); } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index e876bae5f..6ae84ebf4 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -667,7 +667,7 @@ namespace smt { // select(as-array f, i_1, ..., i_n) = (f i_1 ... i_n) // bool theory_array_full::instantiate_select_as_array_axiom(enode* select, enode* arr) { - SASSERT(is_as_array(arr->get_app())); + SASSERT(is_as_array(arr->get_expr())); SASSERT(is_select(select)); SASSERT(arr->get_num_args() == 0); unsigned num_args = select->get_num_args(); @@ -677,12 +677,12 @@ namespace smt { m_stats.m_num_select_as_array_axiom++; ptr_buffer sel_args; - sel_args.push_back(arr->get_app()); + sel_args.push_back(arr->get_expr()); for (unsigned short i = 1; i < num_args; ++i) { sel_args.push_back(select->get_app()->get_arg(i)); } expr * sel = mk_select(sel_args.size(), sel_args.data()); - func_decl * f = array_util(m).get_as_array_func_decl(arr->get_app()); + func_decl * f = array_util(m).get_as_array_func_decl(arr->get_expr()); expr_ref val(m.mk_app(f, sel_args.size()-1, sel_args.data()+1), m); TRACE(array, tout << "new select-as-array axiom...\n"; tout << "as-array: " << mk_bounded_pp(arr->get_expr(), m) << "\n"; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 145650b63..b53583843 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -179,11 +179,15 @@ namespace smt { if (params().m_bv_reflect) { return n->get_arg(idx); } - else { + else if (n->is_app()) { app * arg = to_app(n->get_app()->get_arg(idx)); SASSERT(ctx.e_internalized(arg)); return ctx.get_enode(arg); } + else { + UNREACHABLE(); + return nullptr; + } } inline theory_var theory_bv::get_arg_var(enode * n, unsigned idx) { @@ -1151,7 +1155,7 @@ namespace smt { if (!is_attached_to_var(n) && !approximate_term(n->get_expr())) { mk_bits(mk_var(n)); if (ctx.is_relevant(n)) { - relevant_eh(n->get_app()); + relevant_eh(n->get_expr()); } } } diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 9bcd331b7..247424e18 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -142,10 +142,10 @@ namespace smt { theory_var next(theory_var v) const { return m_find.next(v); } bool is_root(theory_var v) const { return m_find.is_root(v); } unsigned get_bv_size(app const * n) const { return m_util.get_bv_size(n); } - unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_app()); } + unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_expr()); } unsigned get_bv_size(theory_var v) const { return get_bv_size(get_enode(v)); } - bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); } - bool is_bv(enode const* n) const { return is_bv(n->get_app()); } + bool is_bv(expr const* n) const { return m_util.is_bv_sort(n->get_sort()); } + bool is_bv(enode const* n) const { return is_bv(n->get_expr()); } bool is_bv(theory_var v) const { return is_bv(get_enode(v)); } region & get_region() { return m_trail_stack.get_region(); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 6b3428998..3782f54d1 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -171,16 +171,16 @@ namespace smt { func_decl * d = n->get_decl(); ptr_vector const & accessors = *m_util.get_constructor_accessors(d); SASSERT(n->get_num_args() == accessors.size()); - app_ref_vector bindings(m); + expr_ref_vector bindings(m); vector> used_enodes; used_enodes.push_back(std::make_tuple(nullptr, n)); for (unsigned i = 0; i < n->get_num_args(); ++i) { - bindings.push_back(n->get_arg(i)->get_app()); + bindings.push_back(n->get_arg(i)->get_expr()); } unsigned base_id = m.has_trace_stream() && accessors.size() > 0 ? m_util.plugin().get_axiom_base_id(d->get_name()) : 0; unsigned i = 0; for (func_decl * acc : accessors) { - app_ref acc_app(m.mk_app(acc, n->get_app()), m); + app_ref acc_app(m.mk_app(acc, n->get_expr()), m); enode * arg = n->get_arg(i); std::function fn = [&]() { @@ -267,7 +267,7 @@ namespace smt { func_decl * sub_decl = m_util.get_datatype_subterm(s); if (sub_decl) { TRACE(datatype, tout << "asserting reflexivity for #" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << "\n";); - app_ref reflex(m.mk_app(sub_decl, n->get_app(), n->get_app()), m); + app_ref reflex(m.mk_app(sub_decl, n->get_expr(), n->get_expr()), m); ctx.internalize(reflex, false); literal l(ctx.get_bool_var(reflex)); ctx.mark_as_relevant(l); @@ -356,7 +356,7 @@ namespace smt { sort * s = arg->get_sort(); sort *e_sort = nullptr; if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) { - app_ref def(m_autil.mk_default(arg->get_app()), m); + app_ref def(m_autil.mk_default(arg->get_expr()), m); if (!ctx.e_internalized(def)) { ctx.internalize(def, false); } @@ -542,7 +542,7 @@ namespace smt { ptr_vector candidates = list_subterms(arg2); for (enode *s : candidates) { - bool is_leaf = !m_util.is_constructor(s->get_app()); + bool is_leaf = !m_util.is_constructor(s->get_expr()); // Case 1: Equality check (arg1 == s) // Valid if sorts are compatible. @@ -570,7 +570,7 @@ namespace smt { if (sub_decl) { TRACE(datatype, tout << "adding recursive case: " << mk_pp(arg1->get_expr(), m) << " ⊑ " << mk_pp(s->get_expr(), m) << "\n";); - auto tmp = m.mk_not(m.mk_app(sub_decl, arg1->get_app(), s->get_app())); + auto tmp = m.mk_not(m.mk_app(sub_decl, arg1->get_expr(), s->get_expr())); lits.push_back(mk_literal(tmp)); found_possible = true; } @@ -617,7 +617,7 @@ namespace smt { ptr_vector candidates = list_subterms(arg2); for (enode *s : candidates) { - bool is_leaf = !m_util.is_constructor(s->get_app()); + bool is_leaf = !m_util.is_constructor(s->get_expr()); if (s->get_sort() == arg1->get_sort()) { TRACE(datatype, @@ -638,7 +638,7 @@ namespace smt { if (sub_decl) { TRACE(datatype, tout << "asserting NOT " << mk_pp(arg1->get_expr(), m) << " subterm " << mk_pp(s->get_expr(), m) << "\n";); - auto sub_app = m.mk_app(sub_decl, arg1->get_app(), s->get_app()); + auto sub_app = m.mk_app(sub_decl, arg1->get_expr(), s->get_expr()); literal sub_lit = mk_literal(sub_app); literal lits[2] = {antecedent, ~sub_lit}; ctx.mk_th_axiom(get_id(), 2, lits); @@ -678,7 +678,7 @@ namespace smt { enode *ctor = nullptr; enode *iter = root; do { - if (f.th.m_util.is_constructor(iter->get_app())) { + if (f.th.m_util.is_constructor(iter->get_expr())) { ctor = iter; break; } @@ -967,7 +967,7 @@ namespace smt { }; for (enode* sib : *n) { - if (m_sutil.str.is_concat_of_units(sib->get_app())) { + if (m_sutil.str.is_concat_of_units(sib->get_expr())) { add_todo(sib); sibling = sib; break; @@ -994,7 +994,7 @@ namespace smt { theory_array* th = dynamic_cast(ctx.get_theory(m_autil.get_family_id())); for (enode* p : th->parent_selects(n)) m_args.push_back(p); - app_ref def(m_autil.mk_default(n->get_app()), m); + app_ref def(m_autil.mk_default(n->get_expr()), m); m_args.push_back(ctx.get_enode(def)); return m_args; } @@ -1328,7 +1328,7 @@ namespace smt { if (!r) { ptr_vector const & constructors = *m_util.get_datatype_constructors(dt); func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]); - auto rec_app = m.mk_app(rec, n->get_app()); + auto rec_app = m.mk_app(rec, n->get_expr()); consequent = mk_literal(rec_app); } else { @@ -1405,7 +1405,7 @@ namespace smt { } } SASSERT(r != nullptr); - app_ref r_app(m.mk_app(r, n->get_app()), m); + app_ref r_app(m.mk_app(r, n->get_expr()), m); TRACE(datatype, tout << "creating split: " << mk_pp(r_app, m) << "\n";); ctx.internalize(r_app, false); bool_var bv = ctx.get_bool_var(r_app); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 2a0246499..2d1909ba7 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -974,10 +974,9 @@ theory_var theory_diff_logic::expand(bool pos, theory_var v, rational & k) enode* e = get_enode(v); rational r; for (;;) { - app* n = e->get_app(); - if (m_util.is_add(n) && n->get_num_args() == 2) { - app* x = to_app(n->get_arg(0)); - app* y = to_app(n->get_arg(1)); + expr *x = nullptr, *y = nullptr; + expr* n = e->get_expr(); + if (m_util.is_add(n, x, y)) { if (m_util.is_numeral(x, r)) { e = ctx.get_enode(y); } diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index f18c8b375..a3cd84853 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -166,7 +166,7 @@ namespace smt { } void apply_sort_cnstr(enode * n, sort * s) override { - auto term = n->get_app(); + auto term = n->get_expr(); if (u().is_finite_sort(term)) { mk_rep(term); } @@ -214,11 +214,12 @@ namespace smt { } } - bool mk_rep(app* n) { - unsigned num_args = n->get_num_args(); + bool mk_rep(expr* n) { + enode * e = nullptr; - for (unsigned i = 0; i < num_args; ++i) { - ctx.internalize(n->get_arg(i), false); + if (is_app(n)) { + for (auto arg : *to_app(n)) + ctx.internalize(arg, false); } if (ctx.e_internalized(n)) { e = ctx.get_enode(n); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index adedc4fae..40c2cec2a 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -2369,9 +2369,8 @@ namespace smt { model_value_proc * theory_pb::mk_value(enode * n, model_generator & mg) { auto a = n->get_app(); pb_model_value_proc* p = alloc(pb_model_value_proc, a); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - p->add(ctx.get_enode(a->get_arg(i))); - } + for (auto arg : *a) + p->add(ctx.get_enode(arg)); return p; }