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 []
|