145 lines
		
	
	
		
			4.2 KiB
		
	
	
	
		
			OCaml
		
	
	
	
	
	
		
		
			
		
	
	
			145 lines
		
	
	
		
			4.2 KiB
		
	
	
	
		
			OCaml
		
	
	
	
	
	
| 
								 | 
							
								(*
							 | 
						||
| 
								 | 
							
								 * Copyright (c) 1997-1999 Massachusetts Institute of Technology
							 | 
						||
| 
								 | 
							
								 * Copyright (c) 2003, 2007-14 Matteo Frigo
							 | 
						||
| 
								 | 
							
								 * Copyright (c) 2003, 2007-14 Massachusetts Institute of Technology
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * This program is free software; you can redistribute it and/or modify
							 | 
						||
| 
								 | 
							
								 * it under the terms of the GNU General Public License as published by
							 | 
						||
| 
								 | 
							
								 * the Free Software Foundation; either version 2 of the License, or
							 | 
						||
| 
								 | 
							
								 * (at your option) any later version.
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * This program is distributed in the hope that it will be useful,
							 | 
						||
| 
								 | 
							
								 * but WITHOUT ANY WARRANTY; without even the implied warranty of
							 | 
						||
| 
								 | 
							
								 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
							 | 
						||
| 
								 | 
							
								 * GNU General Public License for more details.
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * You should have received a copy of the GNU General Public License
							 | 
						||
| 
								 | 
							
								 * along with this program; if not, write to the Free Software
							 | 
						||
| 
								 | 
							
								 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 *)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(*
							 | 
						||
| 
								 | 
							
								 * the oracle decrees whether the sign of an expression should
							 | 
						||
| 
								 | 
							
								 * be changed.
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * Say the expression (A - B) appears somewhere.  Elsewhere in the
							 | 
						||
| 
								 | 
							
								 * expression dag the expression (B - A) may appear.
							 | 
						||
| 
								 | 
							
								 * The oracle determines which of the two forms is canonical.
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * Algorithm: evaluate the expression at a random input, and
							 | 
						||
| 
								 | 
							
								 * keep the expression with the positive sign.
							 | 
						||
| 
								 | 
							
								 *)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let make_memoizer hash equal =
							 | 
						||
| 
								 | 
							
								  let table = ref Assoctable.empty 
							 | 
						||
| 
								 | 
							
								  in 
							 | 
						||
| 
								 | 
							
								  (fun f k ->
							 | 
						||
| 
								 | 
							
								    match Assoctable.lookup hash equal k !table with
							 | 
						||
| 
								 | 
							
								      Some value -> value
							 | 
						||
| 
								 | 
							
								    | None ->
							 | 
						||
| 
								 | 
							
								        let value = f k in
							 | 
						||
| 
								 | 
							
								        begin	
							 | 
						||
| 
								 | 
							
								          table := Assoctable.insert hash k value !table;
							 | 
						||
| 
								 | 
							
								          value
							 | 
						||
| 
								 | 
							
								        end)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let almost_equal x y = 
							 | 
						||
| 
								 | 
							
								  let epsilon = 1.0E-8 in
							 | 
						||
| 
								 | 
							
								  (abs_float (x -. y) < epsilon) ||
							 | 
						||
| 
								 | 
							
								  (abs_float (x -. y) < epsilon *. (abs_float x +. abs_float y)) 
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let absid = make_memoizer
							 | 
						||
| 
								 | 
							
								    (fun x -> Expr.hash_float (abs_float x))
							 | 
						||
| 
								 | 
							
								    (fun a b -> almost_equal a b || almost_equal (-. a) b)
							 | 
						||
| 
								 | 
							
								    (fun x -> x)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let make_random_oracle () = make_memoizer 
							 | 
						||
| 
								 | 
							
								    Variable.hash 
							 | 
						||
| 
								 | 
							
								    Variable.same
							 | 
						||
| 
								 | 
							
								    (fun _ -> (float (Random.bits())) /. 1073741824.0)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let the_random_oracle = make_random_oracle ()
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let sum_list l = List.fold_right (+.) l 0.0
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let eval_aux random_oracle =
							 | 
						||
| 
								 | 
							
								  let memoizing = make_memoizer Expr.hash (==) in
							 | 
						||
| 
								 | 
							
								  let rec eval x = 
							 | 
						||
| 
								 | 
							
								    memoizing
							 | 
						||
| 
								 | 
							
								      (function
							 | 
						||
| 
								 | 
							
									| Expr.Num x -> Number.to_float x
							 | 
						||
| 
								 | 
							
									| Expr.NaN x -> Expr.transcendent_to_float x
							 | 
						||
| 
								 | 
							
									| Expr.Load v -> random_oracle v
							 | 
						||
| 
								 | 
							
									| Expr.Store (v, x) -> eval x
							 | 
						||
| 
								 | 
							
									| Expr.Plus l -> sum_list (List.map eval l)
							 | 
						||
| 
								 | 
							
									| Expr.Times (a, b) -> (eval a) *. (eval b)
							 | 
						||
| 
								 | 
							
									| Expr.CTimes (a, b) -> 
							 | 
						||
| 
								 | 
							
									    1.098612288668109691395245236 +. 
							 | 
						||
| 
								 | 
							
									       1.609437912434100374600759333 *. (eval a) *. (eval b)
							 | 
						||
| 
								 | 
							
									| Expr.CTimesJ (a, b) -> 
							 | 
						||
| 
								 | 
							
									    0.9102392266268373936142401657 +. 
							 | 
						||
| 
								 | 
							
									      0.6213349345596118107071993881 *. (eval a) *. (eval b)
							 | 
						||
| 
								 | 
							
									| Expr.Uminus x -> -. (eval x))
							 | 
						||
| 
								 | 
							
								      x
							 | 
						||
| 
								 | 
							
								  in eval
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let eval = eval_aux the_random_oracle
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let should_flip_sign node = 
							 | 
						||
| 
								 | 
							
								  let v = eval node in
							 | 
						||
| 
								 | 
							
								  let v' = absid v in
							 | 
						||
| 
								 | 
							
								  not (almost_equal v v')
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(*
							 | 
						||
| 
								 | 
							
								 * determine with high probability if two expressions are equal.
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 * The test is randomized: if the two expressions have the
							 | 
						||
| 
								 | 
							
								 * same value for NTESTS random inputs, then they are proclaimed
							 | 
						||
| 
								 | 
							
								 * equal.  (Note that two distinct linear functions L1(x0, x1, ..., xn)
							 | 
						||
| 
								 | 
							
								 * and L2(x0, x1, ..., xn) have the same value with probability
							 | 
						||
| 
								 | 
							
								 * 0 for random x's, and thus this test is way more paranoid than
							 | 
						||
| 
								 | 
							
								 * necessary.)
							 | 
						||
| 
								 | 
							
								 *)
							 | 
						||
| 
								 | 
							
								let likely_equal a b =
							 | 
						||
| 
								 | 
							
								  let tolerance = 1.0e-8
							 | 
						||
| 
								 | 
							
								  and ntests = 20
							 | 
						||
| 
								 | 
							
								  in
							 | 
						||
| 
								 | 
							
								  let rec loop n =
							 | 
						||
| 
								 | 
							
								    if n = 0 then 
							 | 
						||
| 
								 | 
							
								      true
							 | 
						||
| 
								 | 
							
								    else
							 | 
						||
| 
								 | 
							
								      let r = make_random_oracle () in
							 | 
						||
| 
								 | 
							
								      let va = eval_aux r a
							 | 
						||
| 
								 | 
							
								      and vb = eval_aux r b
							 | 
						||
| 
								 | 
							
								      in
							 | 
						||
| 
								 | 
							
								      if (abs_float (va -. vb)) > 
							 | 
						||
| 
								 | 
							
									   tolerance *. (abs_float va +. abs_float vb +. 0.0001)
							 | 
						||
| 
								 | 
							
								      then
							 | 
						||
| 
								 | 
							
									false
							 | 
						||
| 
								 | 
							
								      else
							 | 
						||
| 
								 | 
							
									loop (n - 1)
							 | 
						||
| 
								 | 
							
								  in
							 | 
						||
| 
								 | 
							
								  match (a, b) with
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								    (* 
							 | 
						||
| 
								 | 
							
								     * Because of the way eval is constructed, we have
							 | 
						||
| 
								 | 
							
								     *     eval (Store (v, x)) == eval x
							 | 
						||
| 
								 | 
							
								     * However, we never consider the two expressions equal
							 | 
						||
| 
								 | 
							
								     *)
							 | 
						||
| 
								 | 
							
								  | (Expr.Store _, _) -> false
							 | 
						||
| 
								 | 
							
								  | (_, Expr.Store _) -> false
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								    (*
							 | 
						||
| 
								 | 
							
								     * Expressions of the form ``Uminus (Store _)''
							 | 
						||
| 
								 | 
							
								     * are artifacts of algsimp
							 | 
						||
| 
								 | 
							
								     *)
							 | 
						||
| 
								 | 
							
								  | ((Expr.Uminus (Expr.Store _)), _) -> false
							 | 
						||
| 
								 | 
							
								  | (_, Expr.Uminus (Expr.Store _)) -> false
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								  | _ -> loop ntests
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let hash x =
							 | 
						||
| 
								 | 
							
								  let f = eval x in
							 | 
						||
| 
								 | 
							
								  truncate (f *. 65536.0)
							 |