why3execute: Adding experimental version of exp and log

bench/interp/real.mlw

@@ -3,6 +3,7 @@ module R
   use real.Real
   use ref.Ref
   use real.Square
+  use real.ExpLog
 
   exception BenchFailure
 
@@ -23,6 +24,18 @@ module R
     let y : real = 1.0 / x in
     (x, y, 3.0 * y)
 
+  let test_exp () =
+    let x: real = 1.0 in
+    exp x
+
+  let test_log () =
+    let x: real = 1.0 in
+    log x
+
+  let test_exp_log () =
+    let x: real = 42.0 in
+    exp (log x), log x, exp x
+
   let bench1 ()
     (* Tries to calculate sqrt(2) *)
     diverges

src/mlw/big_real.ml

@@ -134,7 +134,7 @@ let div x y =
 
 let sqrt (xmin, xmax) =
   set_exponents ();
-  let prec = get_prec() in
+  let prec = get_prec () in
   let zero = get_zero () in
   if lessequal_p zero xmin then
     let res_min = sqrt ~rnd:Toward_Minus_Infinity ~prec xmin in
@@ -143,6 +143,22 @@ let sqrt (xmin, xmax) =
   else
     raise Undetermined
 
+let exp (xmin, xmax) =
+  set_exponents ();
+  let prec = get_prec () in
+  (exp ~rnd:Toward_Minus_Infinity ~prec xmin,
+   exp ~rnd:Toward_Plus_Infinity ~prec xmax)
+
+let log (xmin, xmax) =
+  set_exponents ();
+  let prec = get_prec () in
+  let zero = get_zero () in
+  if lessequal_p zero xmin then
+    (log ~rnd:Toward_Minus_Infinity ~prec xmin,
+     log ~rnd:Toward_Plus_Infinity ~prec xmax)
+  else
+    raise Undetermined
+
 let real_from_str s =
   let prec = get_prec () in
   let n1 = make_from_str ~prec ~base:10 ~rnd:Toward_Minus_Infinity s in

src/mlw/big_real.mli

@@ -17,6 +17,8 @@ val add: real -> real -> real
 val mul: real -> real -> real
 val div: real -> real -> real
 val sqrt: real -> real
+val exp: real -> real
+val log: real -> real
 
 (* Real comparisons *)
 val eq: real -> real -> bool

src/mlw/pinterp.ml

@@ -486,10 +486,16 @@ let built_in_modules =
     ["pi", eval_real Modeconst (Big_real.pi());
     ]
   in
+  let real_exp_log =
+    ["real"], "ExpLog", [],
+    ["exp", eval_real Mode1r Big_real.exp;
+     "log", eval_real Mode1r Big_real.log]
+  in
   bool_module :: (int_modules @ [array_module;
                                  real_module;
                                  real_square_module;
                                  real_trigo_module;
+                                 real_exp_log;
                                  mode_module;
                                  float_modules 32 ~prec:24 "Float32";
                                  float_modules 64 ~prec:53 "Float64";])

src/util/mlmpfr_dummy.ml

@@ -28,6 +28,9 @@ let sub ?rnd:_ ?prec:_ _ _ = raise Not_Implemented
 let abs ?rnd:_ ?prec:_ _ = raise Not_Implemented
 let fma ?rnd:_ ?prec:_ _ _ _ = raise Not_Implemented
 let rint ?rnd:_ ?prec:_ _ = raise Not_Implemented
+let exp ?rnd:_ ?prec:_ _ = raise Not_Implemented
+let log ?rnd:_ ?prec:_ _ = raise Not_Implemented
+
 
 let min ?rnd:_ ?prec:_ _ _ = raise Not_Implemented
 let max ?rnd:_ ?prec:_ _ _ = raise Not_Implemented

src/util/mlmpfr_wrapper.mli

@@ -36,6 +36,8 @@ val sub: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float
 val abs: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
 val fma: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float -> mpfr_float
 val rint: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
+val exp : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
+val log : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
 
 
 val min: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float

stdlib/real.mlw

@@ -228,13 +228,13 @@ module ExpLog
 
   use Real
 
-  function exp real : real
+  val function exp real : real
   axiom Exp_zero : exp(0.0) = 1.0
   axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
 
   constant e : real = exp 1.0
 
-  function log real : real
+  val function log real : real
   axiom Log_one : log 1.0 = 0.0
   axiom Log_mul :
     forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y

[MARCHE Claude]

il faut less_p ici, car log 0 n'est pas defini

[DAILLER Sylvain]

fixed