mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-04 08:16:17 +00:00
Code Activity

Add std::initializer_list overloads for BV and arith operations (#8467)

Browse source 
* 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>
This commit is contained in:
Copilot 2026-02-02 10:00:13 -08:00 • committed by GitHub
parent 20e19b97ee
commit 50d04d32bf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 26 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/arith_decl_plugin.h
View file

@ -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<expr*> 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<expr*> 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<expr*> 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<expr*> 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); }

4
src/ast/bv_decl_plugin.h
View file

@ -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<expr*> 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<expr> const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); }
app * mk_concat(ptr_vector<expr> 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<expr*> 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<expr*> 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<expr*> 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); }

48
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);

3
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -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));
}
}

5
src/test/expr_substitution.cpp
View file

@ -16,10 +16,7 @@ Copyright (c) 2015 Microsoft Corporation
#include <iostream>
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) {