From 76ad2fde8a9bcf37c000e50df22d4785332c4853 Mon Sep 17 00:00:00 2001 From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com> Date: Fri, 10 Nov 2023 17:54:05 -0500 Subject: [PATCH 1/2] Let from_i64 use Into --- z3/src/ast.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 6667260c..04560d76 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -773,9 +773,9 @@ impl<'ctx> Int<'ctx> { } } - pub fn from_i64(ctx: &'ctx Context, i: i64) -> Int<'ctx> { + pub fn from_i64>(ctx: &'ctx Context, i: T) -> Int<'ctx> { let sort = Sort::int(ctx); - unsafe { Self::wrap(ctx, Z3_mk_int64(ctx.z3_ctx, i, sort.z3_sort)) } + unsafe { Self::wrap(ctx, Z3_mk_int64(ctx.z3_ctx, i.into(), sort.z3_sort)) } } pub fn from_u64(ctx: &'ctx Context, u: u64) -> Int<'ctx> { @@ -1217,9 +1217,9 @@ impl<'ctx> BV<'ctx> { } } - pub fn from_i64(ctx: &'ctx Context, i: i64, sz: u32) -> BV<'ctx> { + pub fn from_i64>(ctx: &'ctx Context, i: T, sz: u32) -> BV<'ctx> { let sort = Sort::bitvector(ctx, sz); - unsafe { Self::wrap(ctx, Z3_mk_int64(ctx.z3_ctx, i, sort.z3_sort)) } + unsafe { Self::wrap(ctx, Z3_mk_int64(ctx.z3_ctx, i.into(), sort.z3_sort)) } } pub fn from_u64(ctx: &'ctx Context, u: u64, sz: u32) -> BV<'ctx> { From c3239474460b4ed384cb3dceff605a566f6a1b15 Mon Sep 17 00:00:00 2001 From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com> Date: Fri, 10 Nov 2023 17:54:32 -0500 Subject: [PATCH 2/2] Create an all_num_versions macro --- z3/src/ops.rs | 79 ++++++++++++++++----------------------------------- 1 file changed, 25 insertions(+), 54 deletions(-) diff --git a/z3/src/ops.rs b/z3/src/ops.rs index 30b5fb98..96087b2c 100644 --- a/z3/src/ops.rs +++ b/z3/src/ops.rs @@ -180,6 +180,19 @@ macro_rules! impl_binary_op_bool { }; } +macro_rules! all_num_versions { + ($macro_id:ident, $ty:ty, $($rest:tt)*) => { + $macro_id!($ty, u64, from_u64, $($rest)*); +/* $macro_id!($ty, u32, from_u64, $($rest)*); + $macro_id!($ty, u16, from_u64, $($rest)*); + $macro_id!($ty, u8, from_u64, $($rest)*); */ + $macro_id!($ty, i64, from_i64, $($rest)*); + $macro_id!($ty, i32, from_i64, $($rest)*); + $macro_id!($ty, i16, from_i64, $($rest)*); + $macro_id!($ty, i8, from_i64, $($rest)*); + } +} + macro_rules! impl_binary_op { ($ty:ty, $base_trait:ident, $assign_trait:ident, $base_fn:ident, $assign_fn:ident, $function:ident, $construct_constant:ident) => { impl_binary_op_without_numbers!( @@ -190,32 +203,10 @@ macro_rules! impl_binary_op { $assign_fn, $function ); - impl_binary_op_assign_number_raw!( - $ty, - u64, - from_u64, - $ty, - $base_trait, - $assign_trait, - $base_fn, - $assign_fn, - $function, - $construct_constant - ); - impl_binary_op_number_raw!( - &$ty, - u64, - from_u64, - $ty, - $base_trait, - $base_fn, - $function, - $construct_constant - ); - impl_binary_op_assign_number_raw!( + + all_num_versions!( + impl_binary_op_assign_number_raw, $ty, - i64, - from_i64, $ty, $base_trait, $assign_trait, @@ -224,10 +215,10 @@ macro_rules! impl_binary_op { $function, $construct_constant ); - impl_binary_op_number_raw!( + + all_num_versions!( + impl_binary_op_number_raw, &$ty, - i64, - from_i64, $ty, $base_trait, $base_fn, @@ -408,30 +399,10 @@ macro_rules! impl_binary_mult_op { $base_fn, $assign_fn ); - impl_binary_mult_op_assign_number_raw!( - $ty, - u64, - from_u64, - $ty, - $base_trait, - $assign_trait, - $base_fn, - $assign_fn, - $construct_constant - ); - impl_binary_mult_op_number_raw!( - &$ty, - u64, - from_u64, - $ty, - $base_trait, - $base_fn, - $construct_constant - ); - impl_binary_mult_op_assign_number_raw!( + + all_num_versions!( + impl_binary_mult_op_assign_number_raw, $ty, - i64, - from_i64, $ty, $base_trait, $assign_trait, @@ -439,10 +410,10 @@ macro_rules! impl_binary_mult_op { $assign_fn, $construct_constant ); - impl_binary_mult_op_number_raw!( + + all_num_versions!( + impl_binary_mult_op_number_raw, &$ty, - i64, - from_i64, $ty, $base_trait, $base_fn,