feat: exact f64 from Real

prove-rs · Aug 2, 2024 · 2f32da9 · 2f32da9
1 parent 42bae5f
commit 2f32da9
Showing 1 changed file with 14 additions and 0 deletions.
diff --git 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)) }
     }