Add binding for FPA to IEEE-754 bit-vector (#322)

prove-rs · Nov 7, 2024 · cb10013 · cb10013
1 parent ea9df51
commit cb10013
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/z3/src/ast.rs b/z3/src/ast.rs
@@ -1132,6 +1132,11 @@ 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);