From af9841122b77118d69b4c96804fe2d720c0addf8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 7 Feb 2026 13:12:21 +0000 Subject: [PATCH] Refactor mk_or and mk_and helpers to use std::initializer_list Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/ast.h | 3 ++- src/ast/ast_util.cpp | 2 +- src/ast/ast_util.h | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index d96958a3d..52aca7aad 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 @@ -2210,7 +2211,7 @@ public: app * mk_or(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_OR, arg1, arg2); } app * mk_and(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_AND, arg1, arg2); } app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_OR, arg1, arg2, arg3); } - app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(basic_family_id, OP_OR, 4, args); } + app * mk_or(std::initializer_list args) { return mk_app(basic_family_id, OP_OR, static_cast(args.size()), args.begin()); } app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_AND, arg1, arg2, arg3); } app * mk_and(ref_vector const& args) { return mk_and(std::span(args.data(), args.size())); } diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 5d71ffda9..fa68cf2ec 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -177,7 +177,7 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) { else if (num_args == 1) return args[0]; else - return m.mk_or(num_args, args); + return m.mk_or(std::span(args, num_args)); } app* mk_or(ast_manager & m, unsigned num_args, app * const * args) { diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 3bddac833..e23bc6d34 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -103,7 +103,7 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args); app * mk_and(ast_manager & m, unsigned num_args, app * const * args); inline expr * mk_and(ast_manager & m, ptr_vector const& args) { return mk_and(m, args.size(), args.data()); } inline expr * mk_and(ast_manager & m, ptr_buffer const& args) { return mk_and(m, args.size(), args.data()); } -inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); } +inline expr * mk_and(ast_manager & m, std::initializer_list args) { return mk_and(m, static_cast(args.size()), args.begin()); } inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); } inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); } @@ -125,7 +125,7 @@ app_ref operator+(expr_ref& a, expr_ref& b); */ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args); app * mk_or(ast_manager & m, unsigned num_args, app * const * args); -inline expr * mk_or(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_or(m, 2, args); } +inline expr * mk_or(ast_manager & m, std::initializer_list args) { return mk_or(m, static_cast(args.size()), args.begin()); } inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); } inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); }