feat: expose float to ieee-754 bv conversion

prove-rs · Nov 7, 2024 · 018e963 · 018e963
1 parent ea9df51
commit 018e963
Showing 1 changed file with 10 additions and 0 deletions.
diff --git 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);