From fb043ac9eef7464dba061e9f43aba2c9c3f9b588 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:28:31 +0000 Subject: [PATCH] Add std::initializer_list overloads for update_quantifier and update call sites Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/ast.cpp | 9 +++++++++ src/ast/ast.h | 7 +++++++ src/ast/macros/macro_finder.cpp | 12 ++++-------- 3 files changed, 20 insertions(+), 8 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4aeda7a5c..1583fb4ec 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2588,6 +2588,15 @@ quantifier * ast_manager::update_quantifier(quantifier * q, quantifier_kind k, u num_patterns == 0 ? q->get_no_patterns() : nullptr); } +quantifier * ast_manager::update_quantifier(quantifier * q, std::initializer_list patterns, expr * body) { + return update_quantifier(q, static_cast(patterns.size()), patterns.begin(), body); +} + +quantifier * ast_manager::update_quantifier(quantifier * q, std::initializer_list patterns, std::initializer_list no_patterns, expr * body) { + return update_quantifier(q, static_cast(patterns.size()), patterns.begin(), + static_cast(no_patterns.size()), no_patterns.begin(), body); +} + app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_DISTINCT, num_args, args); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 6e5ce8c78..f081fc57f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -49,6 +49,7 @@ Revision History: #include "util/rlimit.h" #include #include +#include #define RECYCLE_FREE_AST_INDICES @@ -2071,6 +2072,12 @@ public: quantifier * update_quantifier(quantifier * q, quantifier_kind new_kind, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body); + // Convenience overloads with std::initializer_list + [[nodiscard]] quantifier * update_quantifier(quantifier * q, std::initializer_list new_patterns, expr * new_body); + + [[nodiscard]] quantifier * update_quantifier(quantifier * q, std::initializer_list new_patterns, std::initializer_list new_no_patterns, expr * new_body); + + // ----------------------------------- // // expr_array diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index f9b50a062..c6dcf8450 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -97,8 +97,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, bool deps_valid, expr_de expr * body1 = m.mk_eq(head, new_rhs2); expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); quantifier * q1 = m.update_quantifier(new_q, body1); - expr * patterns[1] = { m.mk_pattern(k_app) }; - quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2); + quantifier * q2 = m.update_quantifier(new_q, { m.mk_pattern(k_app) }, body2); new_exprs.push_back(q1); new_exprs.push_back(q2); if (m.proofs_enabled()) { @@ -169,8 +168,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector& expr * body1 = m.mk_eq(head, new_rhs2); expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); quantifier * q1 = m.update_quantifier(new_q, body1); - expr * patterns[1] = { m.mk_pattern(k_app) }; - quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2); + quantifier * q2 = m.update_quantifier(new_q, { m.mk_pattern(k_app) }, body2); proof* pr1 = nullptr, *pr2 = nullptr; if (m.proofs_enabled()) { // new_pr : new_q @@ -210,8 +208,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e app * body_1 = m.mk_eq(head, ite); app * body_2 = m.mk_not(m.mk_eq(k_app, t)); quantifier * q1 = m.update_quantifier(q, body_1); - expr * pats[1] = { m.mk_pattern(k_app) }; - quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns + quantifier * q2 = m.update_quantifier(q, { m.mk_pattern(k_app) }, body_2); // erase patterns new_exprs.push_back(q1); new_exprs.push_back(q2); if (m.proofs_enabled()) { @@ -244,8 +241,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e app * body_2 = m.mk_not(m.mk_eq(k_app, t)); quantifier * q1 = m.update_quantifier(q, body_1); proof * pr1 = nullptr, *pr2 = nullptr; - expr * pats[1] = { m.mk_pattern(k_app) }; - quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns + quantifier * q2 = m.update_quantifier(q, { m.mk_pattern(k_app) }, body_2); // erase patterns if (m.proofs_enabled()) { // r : [rewrite] q ~ q1 & q2 // pr : q