-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathdichotomy_test.ml
122 lines (107 loc) · 3.05 KB
/
dichotomy_test.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
open Dichotomy
(*
let max3 = max_float /. 3.
let check_invariant a b =
match range a b with
| Range (l, u) ->
let b1 = l +. a = b in
let b2 = u +. a = b in
let b3 =
if l <> (-.max_float) then
(if l > 0. then (fpred l) else (fsucc l)) +. a <> b
else
true in
let b4 =
if u <> max_float then
(if u > 0. then (fsucc u) else (fpred u)) +. a <> b
else
true in
if not (b1 && b2 && b3 && b4) then failwith "Err1" else ()
| Single s ->
if (not ((fsucc s) +. a <> b) && ((fpred s) +. a <> b)) then
failwith "Err2" else ()
| Empty ->
if b <> infinity && b <> neg_infinity && (b -. a) +. a = b then
failwith "Err3" else ()
let test a b =
try
check_invariant a b
with _ ->
Printf.printf "f1: %.16e\nf2: %.16e\n" a b;
print_endline (range a b |> to_string);
ignore (dump a b); assert false
let normal_test () =
test 1.0 1.0;
test 1.0 1.1;
test 1.0 1.2;
test 1.0 1.4;
test 1.0 1.5;
test 0.0 1.3;
test 0.0 1.4;
test 0.0 1.5;
test 0.0 1.6;
test 0.0 1.7;
test max_float infinity;
test (max_float /. 3.) infinity;
test (max_float /. 2.) infinity;
test (max_float /. 2.) max_float;
test (max_float /. 2.) (max_float /. 3.)
let () = Random.self_init ()
let random_pos () =
match Random.int 20 with
| 0 -> min_float
| 1 -> max_float
| 2 -> Random.float min_float
| 3 | 4 -> Random.float max_float
| 5 -> Random.float 2e-308
| 6 -> 2e-308
| 7 | 8 | 9 -> Random.float 100.
(*
| 11 | 12 -> 0.0
*)
| 13 -> max_float /. 2.
| 14 -> max_float /. 3.
| 15 | 16 -> (float_of_int @@ Random.int 100) /. 10.
| _ -> Random.float 1_000_00.
let random_pair () =
let a = random_pos () in
let b = if Random.int 10 < 2 then infinity else random_pos () in
let a = if Random.bool () then a else (-. a) in
let b = if Random.bool () then b else (-. b) in
if Random.int 5 < 1 then a, a else a, b
let random_test () =
for i = 0 to 100000 do
let f1, f2 = random_pair () in
test f1 f2
done
(*
let () = normal_test ()
let () = random_test ()
*)
let rtest1 () =
let test () =
let l = random_pos () in
let u = l +. Random.float (max_float -. l) in
let x = upper_pos l u in
if l +. x <= u then () else (Printf.printf "%.16e %.16e\n" l u; assert false);
if l +. (fsucc x) > u then () else (Printf.printf "%.16e %.16e\n" l u; assert false) in
for i = 0 to 1000000000 do
test ()
done
let chech2 l u =
let x = fsucc @@ upper_neg u l in
if l +. x <= u then () else (Printf.printf "%.16e %.16e\n" u l; assert false);
if l +. (fpred x) > u then () else (Printf.printf "%.16e %.16e\n" u l; assert false)
let rtest2 () =
let test () =
let l = random_pos () in
let u = l +. Random.float (max_float -. l) in
let x = fsucc @@ upper_neg u l in
if l +. x <= u then () else (Printf.printf "%.16e %.16e\n" u l; assert false);
if l +. (fpred x) > u then () else (Printf.printf "%.16e %.16e\n" u l; assert false) in
for i = 0 to 1000000000 do
test ()
done
let () = rtest2 ()
*)
(* {0.4 ... 1.8} {0.4 ... 1.8} *)