From ea5da68d6b51a5e237c8c9262c8f9b9095e50012 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 14 May 2024 14:46:39 +0200
Subject: [PATCH] Convert floating point to Why3 term more efficiently
---
src/transformations/utils.ml | 22 ++++++++++------------
1 file changed, 10 insertions(+), 12 deletions(-)
diff --git a/src/transformations/utils.ml b/src/transformations/utils.ml
index 659bd88..ad9e5e4 100644
--- a/src/transformations/utils.ml
+++ b/src/transformations/utils.ml
@@ -35,19 +35,17 @@ let float_of_real_constant rc =
if is_neg then Float.neg f else f
let real_constant_of_float value =
- let neg = Float.is_negative value in
- let value = Fmt.str "%.64f" (Float.abs value) in
- (* Split into integer and fractional parts. *)
- let int_frac = String.split value ~on:'.' in
- let int = List.hd_exn int_frac in
- let frac =
- match List.tl_exn int_frac with
- | [] -> ""
- | [ s ] -> s
- | _ -> assert false (* Since every float has one '.' at most. *)
- in
+ assert (Float.is_finite value);
+ let m, e = Float.frexp value in
+ (* put into the form m * 2^e, where m is an integer *)
+ let m, e = (Int.of_float (Float.ldexp m 53), e - 53) in
Why3.Constant.ConstReal
- (Why3.Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+ {
+ rl_kind = RLitDec 0;
+ rl_real =
+ Why3.Number.real_value ~pow2:(Why3.BigInt.of_int e)
+ (Why3.BigInt.of_int m);
+ }
let term_of_float env f =
let th = Symbols.Float64.create env in
--
GitLab