feat: Real ast as f64

prove-rs · Mar 29, 2024 · 1d38944 · 1d38944
1 parent 38cb5e5
commit 1d38944
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/z3/src/ast.rs b/z3/src/ast.rs
@@ -937,6 +937,12 @@ impl<'ctx> Real<'ctx> {
         }
     }
 
+    pub fn as_f64(&self) -> f64 {
+        unsafe {
+            Z3_get_numeral_double(self.ctx.z3_ctx, self.z3_ast)
+        }
+    }
+
     pub fn from_int(ast: &Int<'ctx>) -> Real<'ctx> {
         unsafe { Self::wrap(ast.ctx, Z3_mk_int2real(ast.ctx.z3_ctx, ast.z3_ast)) }
     }