From 018e96372a8ac5be5d9ed1ef7efbbe4075cbf1b8 Mon Sep 17 00:00:00 2001 From: KpwnZ <22996989+KpwnZ@users.noreply.github.com> Date: Wed, 6 Nov 2024 20:48:30 -0800 Subject: [PATCH] feat: expose float to ieee-754 bv conversion --- z3/src/ast.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 93caf759..9cdf17fc 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -1132,6 +1132,16 @@ impl<'ctx> Float<'ctx> { Self::round_towards_zero(self.ctx).div(self, other) } + // Convert to IEEE-754 bit-vector + pub fn to_ieee_bv(&self) -> BV<'ctx> { + unsafe { + BV::wrap( + self.ctx, + Z3_mk_fpa_to_ieee_bv(self.ctx.z3_ctx, self.z3_ast), + ) + } + } + unop! { unary_abs(Z3_mk_fpa_abs, Self); unary_neg(Z3_mk_fpa_neg, Self);