From 2f32da93b697a322cc3830132ad14f21ddef2a01 Mon Sep 17 00:00:00 2001
From: Lucas Van Laer <lucas.van.laer@gmail.com>
Date: Fri, 2 Aug 2024 12:12:27 +0200
Subject: [PATCH] feat: exact f64 from Real

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

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index a52de25b..57a4bcd3 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -946,6 +946,20 @@ impl<'ctx> Real<'ctx> {
         self.approx(17).parse().unwrap() // 17 decimal digits needed to get full f64 precision
     }
 
+    pub fn exact_f64(&self) -> Option<f64> {
+        let res = unsafe { Z3_get_numeral_double(self.get_ctx().z3_ctx, self.z3_ast) };
+        if res == 0.0 {
+            let mut sacrifice_int = 0;
+            let int_res = unsafe {
+                Z3_get_numeral_int(self.get_ctx().z3_ctx, self.z3_ast, &mut sacrifice_int)
+            };
+            if !int_res || sacrifice_int != 0 {
+                return None;
+            }
+        }
+        return Some(res);
+    }
+
     pub fn from_int(ast: &Int<'ctx>) -> Real<'ctx> {
         unsafe { Self::wrap(ast.ctx, Z3_mk_int2real(ast.ctx.z3_ctx, ast.z3_ast)) }
     }