From 50d04d32bff5ba458136a2b77759449873e370e3 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Feb 2026 10:00:13 -0800 Subject: [PATCH] Add std::initializer_list overloads for BV and arith operations (#8467) * Initial plan * Add std::initializer_list overloads for BV and arith functions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update call sites to use initializer_list format for BV and arith functions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/arith_decl_plugin.h | 4 +++ src/ast/bv_decl_plugin.h | 4 +++ src/ast/fpa/fpa2bv_converter.cpp | 48 +++++++++------------------ src/tactic/fd_solver/smtfd_solver.cpp | 3 +- src/test/expr_substitution.cpp | 5 +-- 5 files changed, 26 insertions(+), 38 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 9dbaeeccd..a57d7ce07 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -503,9 +503,13 @@ public: app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); } + app* mk_band(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, args.size(), args.begin()); } app* mk_shl(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, 2, args); } + app* mk_shl(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, args.size(), args.begin()); } app* mk_ashr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, 2, args); } + app* mk_ashr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, args.size(), args.begin()); } app* mk_lshr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, 2, args); } + app* mk_lshr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, args.size(), args.begin()); } app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 6e4858c20..3a4b50c9e 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -500,13 +500,17 @@ public: return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n); } app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args); } + app * mk_concat(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_CONCAT, args.size(), args.begin()); } app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(expr_ref_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(ptr_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(ptr_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args); } + app * mk_bv_or(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BOR, args.size(), args.begin()); } app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args); } + app * mk_bv_and(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BAND, args.size(), args.begin()); } app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args); } + app * mk_bv_xor(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BXOR, args.size(), args.begin()); } app * mk_concat(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_concat(2, args); } app * mk_bv_and(expr* x, expr* y) { expr* args[2] = { x, y }; return mk_bv_and(2, args); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index afed97a7b..8440104e8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -492,8 +492,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky); SASSERT(is_well_sorted(m, sticky)); - expr * or_args[2] = { shifted_d_sig, sticky }; - shifted_d_sig = m_bv_util.mk_bv_or(2, or_args); + shifted_d_sig = m_bv_util.mk_bv_or({shifted_d_sig, sticky}); SASSERT(is_well_sorted(m, shifted_d_sig)); expr_ref eq_sgn(m); @@ -538,8 +537,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_c_sgn, d_sgn, sign_bv); res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, not_d_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; - res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); + res_sgn = m_bv_util.mk_bv_or({res_sgn_c1, res_sgn_c2, res_sgn_c3}); expr_ref res_sig_eq(m), sig_abs(m), one_1(m); one_1 = m_bv_util.mk_numeral(1, 1); @@ -832,8 +830,7 @@ void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref & b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); expr_ref res_sgn(m), res_sig(m), res_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - res_sgn = m_bv_util.mk_bv_xor(2, signs); + res_sgn = m_bv_util.mk_bv_xor({a_sgn, b_sgn}); dbg_decouple("fpa2bv_mul_res_sgn", res_sgn); @@ -981,8 +978,7 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); expr_ref res_sgn(m), res_sig(m), res_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - res_sgn = m_bv_util.mk_bv_xor(2, signs); + res_sgn = m_bv_util.mk_bv_xor({a_sgn, b_sgn}); expr_ref a_lz_ext(m), b_lz_ext(m); a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); @@ -1569,9 +1565,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_c_lz", c_lz_ext); expr_ref mul_sgn(m), mul_sig(m), mul_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - mul_sgn = m_bv_util.mk_bv_xor(2, signs); + mul_sgn = m_bv_util.mk_bv_xor({a_sgn, b_sgn}); dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn); mul_exp = m_bv_util.mk_bv_add( @@ -1711,8 +1706,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv); res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; - res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); + res_sgn = m_bv_util.mk_bv_or({res_sgn_c1, res_sgn_c2, res_sgn_c3}); dbg_decouple("fpa2bv_fma_res_sgn", res_sgn); expr_ref is_sig_neg(m); @@ -1757,8 +1751,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, sticky_h1 = m_bv_util.mk_extract(sbits+too_short-2, 0, sig_abs); sig_abs_h1 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits-1+too_short, sig_abs); sticky_h1_red = m_bv_util.mk_zero_extend(sbits+5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); - expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red }; - sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args); + sig_abs_h1_f = m_bv_util.mk_bv_or({sig_abs_h1, sticky_h1_red}); res_sig_1 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h1_f); SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits+too_short-1); SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits+6); @@ -1770,8 +1763,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, sticky_h2 = m_bv_util.mk_extract(sbits+too_short-1, 0, sig_abs); sig_abs_h2 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits+too_short, sig_abs); sticky_h2_red = m_bv_util.mk_zero_extend(sbits+4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); - expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red }; - sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args)); + sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or({sig_abs_h2, sticky_h2_red})); res_sig_2 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h2_f); SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits+too_short); SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits+5); @@ -1921,9 +1913,8 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T); m_simp.mk_eq(T_lsds5, one1, t_lt_0); - expr * or_args[2] = { Q, S }; expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m); - Q_or_S = m_bv_util.mk_bv_or(2, or_args); + Q_or_S = m_bv_util.mk_bv_or({Q, S}); m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q); R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1); T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T); @@ -1945,8 +1936,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, last_ext = m_bv_util.mk_zero_extend(sbits + 3, last); one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4); m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky); - expr * or_args[2] = { rest_ext, sticky }; - res_sig = m_bv_util.mk_bv_or(2, or_args); + res_sig = m_bv_util.mk_bv_or({rest_ext, sticky}); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); @@ -3976,25 +3966,20 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr); expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m); - expr * last_sticky[2] = { last, sticky }; - expr * round_sticky[2] = { round, sticky }; - last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky); - round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); + last_or_sticky = m_bv_util.mk_bv_or({last, sticky}); + round_or_sticky = m_bv_util.mk_bv_or({round, sticky}); not_last = m_bv_util.mk_bv_not(last); not_round = m_bv_util.mk_bv_not(round); not_sticky = m_bv_util.mk_bv_not(sticky); not_lors = m_bv_util.mk_bv_not(last_or_sticky); not_rors = m_bv_util.mk_bv_not(round_or_sticky); not_sgn = m_bv_util.mk_bv_not(sgn); - expr * nround_lors[2] = { not_round, not_lors }; - expr * pos_args[2] = { sgn, not_rors }; - expr * neg_args[2] = { not_sgn, not_rors }; expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m); - inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nround_lors)); + inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or({not_round, not_lors})); inc_taway = round; - inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args)); - inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); + inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or({sgn, not_rors})); + inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or({not_sgn, not_rors})); expr_ref res(m), inc_c2(m), inc_c3(m), inc_c4(m); expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m); @@ -4158,8 +4143,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & // put the sticky bit into the significand. expr_ref ext_sticky(m); ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky); - expr * tmp[2] = { sig, ext_sticky }; - sig = m_bv_util.mk_bv_or(2, tmp); + sig = m_bv_util.mk_bv_or({sig, ext_sticky}); SASSERT(is_well_sorted(m, sig)); SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 6d4963c0d..8b765a04e 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -188,8 +188,7 @@ namespace smtfd { } unsigned n = (m_rand() << 16) | m_rand(); expr* num = m_butil.mk_numeral(n, bw); - expr* es[2] = { num, m.mk_fresh_const(name, m_butil.mk_sort(bw)) }; - expr* e = m_butil.mk_bv_xor(2, es); + expr* e = m_butil.mk_bv_xor({num, m.mk_fresh_const(name, m_butil.mk_sort(bw))}); return m_butil.mk_concat(e, m_butil.mk_numeral(0, 24 - bw)); } } diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp index a1a8d7e4e..33f4a201c 100644 --- a/src/test/expr_substitution.cpp +++ b/src/test/expr_substitution.cpp @@ -16,10 +16,7 @@ Copyright (c) 2015 Microsoft Corporation #include expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) { - expr* args[2]; - args[0] = a; - args[1] = b; - return bv.mk_bv_xor(2, args); + return bv.mk_bv_xor({a, b}); } expr* mk_bv_and(bv_util& bv, expr* a, expr* b) {