cannam@95
|
1 (*
|
cannam@95
|
2 * Copyright (c) 1997-1999 Massachusetts Institute of Technology
|
cannam@95
|
3 * Copyright (c) 2003, 2007-11 Matteo Frigo
|
cannam@95
|
4 * Copyright (c) 2003, 2007-11 Massachusetts Institute of Technology
|
cannam@95
|
5 *
|
cannam@95
|
6 * This program is free software; you can redistribute it and/or modify
|
cannam@95
|
7 * it under the terms of the GNU General Public License as published by
|
cannam@95
|
8 * the Free Software Foundation; either version 2 of the License, or
|
cannam@95
|
9 * (at your option) any later version.
|
cannam@95
|
10 *
|
cannam@95
|
11 * This program is distributed in the hope that it will be useful,
|
cannam@95
|
12 * but WITHOUT ANY WARRANTY; without even the implied warranty of
|
cannam@95
|
13 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
cannam@95
|
14 * GNU General Public License for more details.
|
cannam@95
|
15 *
|
cannam@95
|
16 * You should have received a copy of the GNU General Public License
|
cannam@95
|
17 * along with this program; if not, write to the Free Software
|
cannam@95
|
18 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
|
cannam@95
|
19 *
|
cannam@95
|
20 *)
|
cannam@95
|
21
|
cannam@95
|
22 (*
|
cannam@95
|
23 * the oracle decrees whether the sign of an expression should
|
cannam@95
|
24 * be changed.
|
cannam@95
|
25 *
|
cannam@95
|
26 * Say the expression (A - B) appears somewhere. Elsewhere in the
|
cannam@95
|
27 * expression dag the expression (B - A) may appear.
|
cannam@95
|
28 * The oracle determines which of the two forms is canonical.
|
cannam@95
|
29 *
|
cannam@95
|
30 * Algorithm: evaluate the expression at a random input, and
|
cannam@95
|
31 * keep the expression with the positive sign.
|
cannam@95
|
32 *)
|
cannam@95
|
33
|
cannam@95
|
34 let make_memoizer hash equal =
|
cannam@95
|
35 let table = ref Assoctable.empty
|
cannam@95
|
36 in
|
cannam@95
|
37 (fun f k ->
|
cannam@95
|
38 match Assoctable.lookup hash equal k !table with
|
cannam@95
|
39 Some value -> value
|
cannam@95
|
40 | None ->
|
cannam@95
|
41 let value = f k in
|
cannam@95
|
42 begin
|
cannam@95
|
43 table := Assoctable.insert hash k value !table;
|
cannam@95
|
44 value
|
cannam@95
|
45 end)
|
cannam@95
|
46
|
cannam@95
|
47 let almost_equal x y =
|
cannam@95
|
48 let epsilon = 1.0E-8 in
|
cannam@95
|
49 (abs_float (x -. y) < epsilon) ||
|
cannam@95
|
50 (abs_float (x -. y) < epsilon *. (abs_float x +. abs_float y))
|
cannam@95
|
51
|
cannam@95
|
52 let absid = make_memoizer
|
cannam@95
|
53 (fun x -> Expr.hash_float (abs_float x))
|
cannam@95
|
54 (fun a b -> almost_equal a b || almost_equal (-. a) b)
|
cannam@95
|
55 (fun x -> x)
|
cannam@95
|
56
|
cannam@95
|
57 let make_random_oracle () = make_memoizer
|
cannam@95
|
58 Variable.hash
|
cannam@95
|
59 Variable.same
|
cannam@95
|
60 (fun _ -> (float (Random.bits())) /. 1073741824.0)
|
cannam@95
|
61
|
cannam@95
|
62 let the_random_oracle = make_random_oracle ()
|
cannam@95
|
63
|
cannam@95
|
64 let sum_list l = List.fold_right (+.) l 0.0
|
cannam@95
|
65
|
cannam@95
|
66 let eval_aux random_oracle =
|
cannam@95
|
67 let memoizing = make_memoizer Expr.hash (==) in
|
cannam@95
|
68 let rec eval x =
|
cannam@95
|
69 memoizing
|
cannam@95
|
70 (function
|
cannam@95
|
71 | Expr.Num x -> Number.to_float x
|
cannam@95
|
72 | Expr.NaN x -> Expr.transcendent_to_float x
|
cannam@95
|
73 | Expr.Load v -> random_oracle v
|
cannam@95
|
74 | Expr.Store (v, x) -> eval x
|
cannam@95
|
75 | Expr.Plus l -> sum_list (List.map eval l)
|
cannam@95
|
76 | Expr.Times (a, b) -> (eval a) *. (eval b)
|
cannam@95
|
77 | Expr.CTimes (a, b) ->
|
cannam@95
|
78 1.098612288668109691395245236 +.
|
cannam@95
|
79 1.609437912434100374600759333 *. (eval a) *. (eval b)
|
cannam@95
|
80 | Expr.CTimesJ (a, b) ->
|
cannam@95
|
81 0.9102392266268373936142401657 +.
|
cannam@95
|
82 0.6213349345596118107071993881 *. (eval a) *. (eval b)
|
cannam@95
|
83 | Expr.Uminus x -> -. (eval x))
|
cannam@95
|
84 x
|
cannam@95
|
85 in eval
|
cannam@95
|
86
|
cannam@95
|
87 let eval = eval_aux the_random_oracle
|
cannam@95
|
88
|
cannam@95
|
89 let should_flip_sign node =
|
cannam@95
|
90 let v = eval node in
|
cannam@95
|
91 let v' = absid v in
|
cannam@95
|
92 not (almost_equal v v')
|
cannam@95
|
93
|
cannam@95
|
94 (*
|
cannam@95
|
95 * determine with high probability if two expressions are equal.
|
cannam@95
|
96 *
|
cannam@95
|
97 * The test is randomized: if the two expressions have the
|
cannam@95
|
98 * same value for NTESTS random inputs, then they are proclaimed
|
cannam@95
|
99 * equal. (Note that two distinct linear functions L1(x0, x1, ..., xn)
|
cannam@95
|
100 * and L2(x0, x1, ..., xn) have the same value with probability
|
cannam@95
|
101 * 0 for random x's, and thus this test is way more paranoid than
|
cannam@95
|
102 * necessary.)
|
cannam@95
|
103 *)
|
cannam@95
|
104 let likely_equal a b =
|
cannam@95
|
105 let tolerance = 1.0e-8
|
cannam@95
|
106 and ntests = 20
|
cannam@95
|
107 in
|
cannam@95
|
108 let rec loop n =
|
cannam@95
|
109 if n = 0 then
|
cannam@95
|
110 true
|
cannam@95
|
111 else
|
cannam@95
|
112 let r = make_random_oracle () in
|
cannam@95
|
113 let va = eval_aux r a
|
cannam@95
|
114 and vb = eval_aux r b
|
cannam@95
|
115 in
|
cannam@95
|
116 if (abs_float (va -. vb)) >
|
cannam@95
|
117 tolerance *. (abs_float va +. abs_float vb +. 0.0001)
|
cannam@95
|
118 then
|
cannam@95
|
119 false
|
cannam@95
|
120 else
|
cannam@95
|
121 loop (n - 1)
|
cannam@95
|
122 in
|
cannam@95
|
123 match (a, b) with
|
cannam@95
|
124
|
cannam@95
|
125 (*
|
cannam@95
|
126 * Because of the way eval is constructed, we have
|
cannam@95
|
127 * eval (Store (v, x)) == eval x
|
cannam@95
|
128 * However, we never consider the two expressions equal
|
cannam@95
|
129 *)
|
cannam@95
|
130 | (Expr.Store _, _) -> false
|
cannam@95
|
131 | (_, Expr.Store _) -> false
|
cannam@95
|
132
|
cannam@95
|
133 (*
|
cannam@95
|
134 * Expressions of the form ``Uminus (Store _)''
|
cannam@95
|
135 * are artifacts of algsimp
|
cannam@95
|
136 *)
|
cannam@95
|
137 | ((Expr.Uminus (Expr.Store _)), _) -> false
|
cannam@95
|
138 | (_, Expr.Uminus (Expr.Store _)) -> false
|
cannam@95
|
139
|
cannam@95
|
140 | _ -> loop ntests
|
cannam@95
|
141
|
cannam@95
|
142 let hash x =
|
cannam@95
|
143 let f = eval x in
|
cannam@95
|
144 truncate (f *. 65536.0)
|