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)) }
  }