From 5932c43c469f48789387b61610a59357f13a8e29 Mon Sep 17 00:00:00 2001
From: KpwnZ <22996989+KpwnZ@users.noreply.github.com>
Date: Wed, 6 Nov 2024 21:44:56 -0800
Subject: [PATCH 1/3] feat: convert ieee-754 bv to float

---
 z3/src/ast.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index 196cad39..cc4b0bf2 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -1138,6 +1138,16 @@ impl<'ctx> Float<'ctx> {
         unsafe { BV::wrap(self.ctx, Z3_mk_fpa_to_ieee_bv(self.ctx.z3_ctx, self.z3_ast)) }
     }
 
+    // Convert from IEEE-754 bit-vector
+    pub fn from_ieee_bv(bv: &BV<'ctx>, s: &Sort<'ctx>) -> Float<'ctx> {
+        unsafe {
+            Self::wrap(
+                bv.ctx,
+                Z3_mk_fpa_to_fp_bv(bv.ctx.z3_ctx, bv.z3_ast, s.z3_sort),
+            )
+        }
+    }
+
     unop! {
         unary_abs(Z3_mk_fpa_abs, Self);
         unary_neg(Z3_mk_fpa_neg, Self);

From b065290267e76dac1ef013d99a2fe6367938de17 Mon Sep 17 00:00:00 2001
From: KpwnZ <22996989+KpwnZ@users.noreply.github.com>
Date: Wed, 6 Nov 2024 23:18:01 -0800
Subject: [PATCH 2/3] feat: convert to float32 or double directly

---
 z3/src/ast.rs | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index cc4b0bf2..dd55c8c7 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -1148,6 +1148,29 @@ impl<'ctx> Float<'ctx> {
         }
     }
 
+    // Convert from IEEE-754 bit-vector
+    pub fn from_ieee_bv32(bv: &BV<'ctx>) -> Float<'ctx> {
+        let sort = Sort::float32(bv.ctx);
+        unsafe {
+            Self::wrap(
+                bv.ctx,
+                Z3_mk_fpa_to_fp_bv(bv.ctx.z3_ctx, bv.z3_ast, sort.z3_sort),
+            )
+        }
+    }
+
+    // Convert from IEEE-754 bit-vector
+    pub fn from_ieee_bv64(bv: &BV<'ctx>) -> Float<'ctx> {
+        let sort = Sort::double(bv.ctx);
+        unsafe {
+            Self::wrap(
+                bv.ctx,
+                Z3_mk_fpa_to_fp_bv(bv.ctx.z3_ctx, bv.z3_ast, sort.z3_sort),
+            )
+        }
+    }
+
+
     unop! {
         unary_abs(Z3_mk_fpa_abs, Self);
         unary_neg(Z3_mk_fpa_neg, Self);

From a4e1f1e96fde5f1fbd43a7f78ef27b35b9033f9a Mon Sep 17 00:00:00 2001
From: kpwnz <22996989+KpwnZ@users.noreply.github.com>
Date: Mon, 21 Jul 2025 18:14:23 -0700
Subject: [PATCH 3/3] chore: format the code

---
 z3/src/ast.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index dd55c8c7..e6ae5f9c 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -1170,7 +1170,6 @@ impl<'ctx> Float<'ctx> {
         }
     }
 
-
     unop! {
         unary_abs(Z3_mk_fpa_abs, Self);
         unary_neg(Z3_mk_fpa_neg, Self);