153 lines
		
	
	
		
			5.3 KiB
		
	
	
	
		
			OCaml
		
	
	
	
	
	
		
		
			
		
	
	
			153 lines
		
	
	
		
			5.3 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
							 | 
						||
| 
								 | 
							
								 *
							 | 
						||
| 
								 | 
							
								 *)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* Here, we define the data type encapsulating a symbolic arithmetic
							 | 
						||
| 
								 | 
							
								   expression, and provide some routines for manipulating it. *)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* I will regret this hack : *)
							 | 
						||
| 
								 | 
							
								(* NEWS: I did *)
							 | 
						||
| 
								 | 
							
								type transcendent = I | MULTI_A | MULTI_B | CONJ
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								type expr =
							 | 
						||
| 
								 | 
							
								  | Num of Number.number
							 | 
						||
| 
								 | 
							
								  | NaN of transcendent
							 | 
						||
| 
								 | 
							
								  | Plus of expr list
							 | 
						||
| 
								 | 
							
								  | Times of expr * expr
							 | 
						||
| 
								 | 
							
								  | CTimes of expr * expr
							 | 
						||
| 
								 | 
							
								  | CTimesJ of expr * expr  (* CTimesJ (a, b) = conj(a) * b *)
							 | 
						||
| 
								 | 
							
								  | Uminus of expr
							 | 
						||
| 
								 | 
							
								  | Load of Variable.variable
							 | 
						||
| 
								 | 
							
								  | Store of Variable.variable * expr
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								type assignment = Assign of Variable.variable * expr
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* various hash functions *)
							 | 
						||
| 
								 | 
							
								let hash_float x = 
							 | 
						||
| 
								 | 
							
								  let (mantissa, exponent) = frexp x
							 | 
						||
| 
								 | 
							
								  in truncate (float_of_int(exponent) *. 1234.567 +. mantissa *. 10000.0)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let sum_list l = List.fold_right (+) l 0
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let transcendent_to_float = function
							 | 
						||
| 
								 | 
							
								  | I -> 2.718281828459045235360287471  (* any transcendent number will do *)
							 | 
						||
| 
								 | 
							
								  | MULTI_A -> 0.6931471805599453094172321214
							 | 
						||
| 
								 | 
							
								  | MULTI_B -> -0.3665129205816643270124391582
							 | 
						||
| 
								 | 
							
								  | CONJ -> 0.6019072301972345747375400015
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let rec hash = function
							 | 
						||
| 
								 | 
							
								  | Num x -> hash_float (Number.to_float x)
							 | 
						||
| 
								 | 
							
								  | NaN x -> hash_float (transcendent_to_float x)
							 | 
						||
| 
								 | 
							
								  | Load v -> 1 + 1237 * Variable.hash v
							 | 
						||
| 
								 | 
							
								  | Store (v, x) -> 2 * Variable.hash v - 2345 * hash x
							 | 
						||
| 
								 | 
							
								  | Plus l -> 5 + 23451 * sum_list (List.map Hashtbl.hash l)
							 | 
						||
| 
								 | 
							
								  | Times (a, b) -> 41 + 31415 * (Hashtbl.hash a +  Hashtbl.hash b)
							 | 
						||
| 
								 | 
							
								  | CTimes (a, b) -> 49 + 3245 * (Hashtbl.hash a +  Hashtbl.hash b)
							 | 
						||
| 
								 | 
							
								  | CTimesJ (a, b) -> 31 + 3471 * (Hashtbl.hash a +  Hashtbl.hash b)
							 | 
						||
| 
								 | 
							
								  | Uminus x -> 42 + 12345 * (hash x)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* find all variables *)
							 | 
						||
| 
								 | 
							
								let rec find_vars x =
							 | 
						||
| 
								 | 
							
								  match x with
							 | 
						||
| 
								 | 
							
								  | Load y -> [y]
							 | 
						||
| 
								 | 
							
								  | Plus l -> List.flatten (List.map find_vars l)
							 | 
						||
| 
								 | 
							
								  | Times (a, b) -> (find_vars a) @ (find_vars b)
							 | 
						||
| 
								 | 
							
								  | CTimes (a, b) -> (find_vars a) @ (find_vars b)
							 | 
						||
| 
								 | 
							
								  | CTimesJ (a, b) -> (find_vars a) @ (find_vars b)
							 | 
						||
| 
								 | 
							
								  | Uminus a -> find_vars a
							 | 
						||
| 
								 | 
							
								  | _ -> []
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* TRUE if expression is a constant *)
							 | 
						||
| 
								 | 
							
								let is_constant = function
							 | 
						||
| 
								 | 
							
								  | Num _ -> true
							 | 
						||
| 
								 | 
							
								  | NaN _ -> true
							 | 
						||
| 
								 | 
							
								  | Load v -> Variable.is_constant v
							 | 
						||
| 
								 | 
							
								  | _ -> false
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let is_known_constant = function
							 | 
						||
| 
								 | 
							
								  | Num _ -> true
							 | 
						||
| 
								 | 
							
								  | NaN _ -> true
							 | 
						||
| 
								 | 
							
								  | _ -> false
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* expr to string, used for debugging *)
							 | 
						||
| 
								 | 
							
								let rec foldr_string_concat l = 
							 | 
						||
| 
								 | 
							
								  match l with
							 | 
						||
| 
								 | 
							
								    [] -> ""
							 | 
						||
| 
								 | 
							
								  | [a] -> a
							 | 
						||
| 
								 | 
							
								  | a :: b -> a ^ " " ^ (foldr_string_concat b)
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let string_of_transcendent = function
							 | 
						||
| 
								 | 
							
								  | I -> "I"
							 | 
						||
| 
								 | 
							
								  | MULTI_A -> "MULTI_A"
							 | 
						||
| 
								 | 
							
								  | MULTI_B -> "MULTI_B"
							 | 
						||
| 
								 | 
							
								  | CONJ -> "CONJ"
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let rec to_string = function
							 | 
						||
| 
								 | 
							
								  | Load v -> Variable.unparse v
							 | 
						||
| 
								 | 
							
								  | Num n -> string_of_float (Number.to_float n)
							 | 
						||
| 
								 | 
							
								  | NaN n -> string_of_transcendent n
							 | 
						||
| 
								 | 
							
								  | Plus x -> "(+ " ^ (foldr_string_concat (List.map to_string x)) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Times (a, b) -> "(* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | CTimes (a, b) -> "(c* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | CTimesJ (a, b) -> "(cj* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Uminus a -> "(- " ^ (to_string a) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Store (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^
							 | 
						||
| 
								 | 
							
								      (to_string a) ^ ")"
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let rec to_string_a d x = 
							 | 
						||
| 
								 | 
							
								  if (d = 0) then "..." else match x with
							 | 
						||
| 
								 | 
							
								  | Load v -> Variable.unparse v
							 | 
						||
| 
								 | 
							
								  | Num n -> Number.to_konst n
							 | 
						||
| 
								 | 
							
								  | NaN n -> string_of_transcendent n
							 | 
						||
| 
								 | 
							
								  | Plus x -> "(+ " ^ (foldr_string_concat (List.map (to_string_a (d - 1)) x)) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Times (a, b) -> "(* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | CTimes (a, b) -> "(c* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | CTimesJ (a, b) -> "(cj* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Uminus a -> "(- " ^ (to_string_a (d-1) a) ^ ")"
							 | 
						||
| 
								 | 
							
								  | Store (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^
							 | 
						||
| 
								 | 
							
								      (to_string_a (d-1) a) ^ ")"
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let to_string = to_string_a 10
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let assignment_to_string = function
							 | 
						||
| 
								 | 
							
								  | Assign (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^ (to_string a) ^ ")"
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let dump print = List.iter (fun x -> print ((assignment_to_string x) ^ "\n"))
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								(* find all constants in a given expression *)
							 | 
						||
| 
								 | 
							
								let rec expr_to_constants = function
							 | 
						||
| 
								 | 
							
								  | Num n -> [n]
							 | 
						||
| 
								 | 
							
								  | Plus a -> List.flatten (List.map expr_to_constants a)
							 | 
						||
| 
								 | 
							
								  | Times (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
							 | 
						||
| 
								 | 
							
								  | CTimes (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
							 | 
						||
| 
								 | 
							
								  | CTimesJ (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
							 | 
						||
| 
								 | 
							
								  | Uminus a -> expr_to_constants a
							 | 
						||
| 
								 | 
							
								  | _ -> []
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let add_float_key_value list_so_far k = 
							 | 
						||
| 
								 | 
							
								  if List.exists (fun k2 -> Number.equal k k2) list_so_far then
							 | 
						||
| 
								 | 
							
								    list_so_far
							 | 
						||
| 
								 | 
							
								  else
							 | 
						||
| 
								 | 
							
								    k :: list_so_far
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								let unique_constants = List.fold_left add_float_key_value [] 
							 |