From 8b87d0a50b866e560c4da820620cf977008a91d6 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 14 Dec 2017 20:57:42 +0100
Subject: [PATCH] Forcing mpfr status when -real mpfr asked. Default precision
is 100 bits.
---
src/options.ml | 2 +-
src/options_management.ml | 11 ++++++++++-
2 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/src/options.ml b/src/options.ml
index 1eca8d39..4ab3b3f6 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -32,7 +32,7 @@ let lusi = ref false
let print_reuse = ref false
let const_unfold = ref false
let mpfr = ref false
-let mpfr_prec = ref 0
+let mpfr_prec = ref 100
let print_dec_types = ref false
let traces = ref false
diff --git a/src/options_management.ml b/src/options_management.ml
index 1a052fb4..bdda79c7 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -66,11 +66,20 @@ let set_mpfr prec =
if prec > 0 then (
mpfr := true;
mpfr_prec := prec;
+ real_type := "mpfr";
(* salsa_enabled := false; (* We deactivate salsa *) TODO *)
)
else
failwith "mpfr requires a positive integer"
+let set_real_type s =
+ match s with
+ "mpfr" -> (
+ mpfr := true;
+ real_type := "mpfr";
+ )
+ | _ -> real_type := s
+
let set_backend s =
output := s;
Backends.setup ()
@@ -113,7 +122,7 @@ let lustrec_options =
"-c++" , Arg.Set cpp , "c++ backend";
"-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
- "-real", Arg.Set_string real_type, "specifies the real type (default=\"double\" without mpfr option)";
+ "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
"-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
"-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";
--
GitLab