Commit 7173bbcb authored by MARCHE Claude's avatar MARCHE Claude

CE for floats: finish handling of binary64, add a decimal printing for humans

parent 896e2144
......@@ -36,13 +36,15 @@ bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000008000000p-1022" } }
"str_hexa" : "-0x1.0000008000000p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000010000000p-1023" } }
"str_hexa" : "-0x0.0000010000000p-1023" ,
"value" : -6.63124e-316 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -54,13 +56,15 @@ bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.4000000000000p0" } }
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.0800000000000p513" } }
"str_hexa" : "0x1.0800000000000p513" ,
"value" : 2.76536e+154 } }
bench/ce/floats.mlw T32 g1 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -100,13 +104,15 @@ bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000008000000p-1022" } }
"str_hexa" : "-0x1.0000008000000p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000010000000p-1023" } }
"str_hexa" : "-0x0.0000010000000p-1023" ,
"value" : -6.63124e-316 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -118,11 +124,13 @@ bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.4000000000000p0" } }
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.0800000000000p513" } }
"str_hexa" : "0x1.0800000000000p513" ,
"value" : 2.76536e+154 } }
......@@ -36,13 +36,15 @@ bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0100000000000p-1022" } }
"str_hexa" : "-0x1.0100000000000p-1022" ,
"value" : -2.23377e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000000000400p-1023" } }
"str_hexa" : "-0x0.0000000000400p-1023" ,
"value" : -2.52962e-321 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -54,13 +56,15 @@ bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.4000000000000p0" } }
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.0000000000001p513" } }
"str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T32 g1 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -100,13 +104,15 @@ bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0100000000000p-1022" } }
"str_hexa" : "-0x1.0100000000000p-1022" ,
"value" : -2.23377e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "-0x1.0000000000400p-1023" } }
"str_hexa" : "-0x0.0000000000400p-1023" ,
"value" : -2.52962e-321 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -118,11 +124,13 @@ bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.4000000000000p0" } }
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"value" : "0x1.0000000000001p513" } }
"str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
......@@ -34,7 +34,7 @@ type float_type =
| Minus_zero
| Not_a_number
| Float_value of string * string * string
| Float_hexa of string
| Float_hexa of string * float
type model_value =
| Integer of string
......@@ -100,9 +100,10 @@ let convert_float_value f =
let m = Mstr.add "exponent" (Json_base.String eb) m in
let m = Mstr.add "significand" (Json_base.String sb) m in
Json_base.Record m
| Float_hexa s ->
| Float_hexa(s,f) ->
let m = Mstr.add "cons" (Json_base.String "Float_hexa") Stdlib.Mstr.empty in
let m = Mstr.add "value" (Json_base.String s) m in
let m = Mstr.add "str_hexa" (Json_base.String s) m in
let m = Mstr.add "value" (Json_base.Float f) m in
Json_base.Record m
let rec convert_model_value value : Json_base.json =
......@@ -206,7 +207,7 @@ let print_float_human fmt f =
fprintf fmt "NaN"
| Float_value (b, eb, sb) ->
fprintf fmt "float_bits(%s,%s,%s)" b eb sb
| Float_hexa s -> fprintf fmt "%s" s
| Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f
let rec print_array_human fmt (arr: model_array) =
fprintf fmt "(";
......
......@@ -22,7 +22,7 @@ type float_type =
| Minus_zero
| Not_a_number
| Float_value of string * string * string
| Float_hexa of string
| Float_hexa of string * float
type model_value =
| Integer of string
......
......@@ -11,6 +11,7 @@
{
open Parse_smtv2_model_parser
open Model_parser
exception SyntaxError
let interp_float b eb sb =
......@@ -20,14 +21,25 @@
| "#b1" -> true
| _ -> raise Exit
in
if String.sub eb 0 2 = "#b" && String.length eb = 13 &&
String.sub sb 0 2 = "#x" && String.length sb = 15 then
if String.length eb = 13 && String.sub eb 0 2 = "#b" &&
String.length sb = 15 && String.sub sb 0 2 = "#x" then
(* binary 64 *)
let exp_base2 = String.sub eb 2 11 in
let exp = int_of_string ("0b" ^ exp_base2) - 1023 in
let mant_base16 = String.sub sb 2 13 in
Model_parser.Float_hexa((if is_neg then "-" else "")^
"0x1."^mant_base16^"p"^(string_of_int exp))
let exp = int_of_string ("0b" ^ exp_base2) in
if exp = 0 then (* subnormals *)
let s = (if is_neg then "-" else "")^
"0x0."^mant_base16^"p-1023"
in Float_hexa(s,float_of_string s)
else if exp = 2047 then (* infinities and NaN *)
if mant_base16="0000000000000" then
if is_neg then Minus_infinity else Plus_infinity
else Not_a_number
else
let exp = exp - 1023 in
let s = (if is_neg then "-" else "")^
"0x1."^mant_base16^"p"^(string_of_int exp)
in Float_hexa(s,float_of_string s)
else
if String.sub eb 0 2 = "#x" && String.length eb = 4 &&
String.sub sb 0 2 = "#b" && String.length eb = 25 then
......@@ -36,7 +48,7 @@
let mant_base2 = String.sub sb 2 23 in
raise Exit (* TODO *)
else raise Exit
with Exit -> Model_parser.Float_value (b, eb, sb)
with Exit -> Float_value (b, eb, sb)
}
let atom = [^'('')'' ''\t''\n']
......
......@@ -52,7 +52,7 @@ let print_float fmt f =
| Model_parser.Minus_zero -> Format.fprintf fmt "Minus_zero"
| Model_parser.Not_a_number -> Format.fprintf fmt "NaN"
| Model_parser.Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
| Model_parser.Float_hexa s -> Format.fprintf fmt "%s" s
| Model_parser.Float_hexa(s,f) -> Format.fprintf fmt "%s (%g)" s f
let rec print_array fmt a =
match a with
......
......@@ -33,7 +33,7 @@ let string fmt s =
let int fmt d = fprintf fmt "%d" d
let bool fmt b = fprintf fmt "%b" b
let float fmt f = fprintf fmt "%f" f
let float fmt f = fprintf fmt "%g" f
(* TODO check that you can print a floating point number like this in JSON *)
let print_json_field key value_pr fmt value =
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment