let mem_stat () =
  let stat = Gc.stat() in
  let word = float_of_int (Sys.word_size / 8) in
  let free = float_of_int stat.Gc.free_words *. word /. 1024.0 in
  let total = float_of_int stat.Gc.heap_words *. word /. 1024.0 in
  let allocated = total -. free in
  let str = sprintf "allocated = %f (free = %f; total_size = %f; %f)\n" 
    allocated free total (free /. total) in
    print_string str;;


(* allocated = 85862 *)
mem_stat();;

Gc.set { (Gc.get()) with Gc.verbose = 0x05 };;
Gc.compact();;

(* allocated = 60243 *)
mem_stat();;




flyspeck_needs "../formal_lp/formal_interval/m_verifier.hl";;

(* allocated = 129006 *)
mem_stat();;

Gc.compact();;
(* allocated = 80510 *)
mem_stat();;

Arith_cache.print_stat();;
Arith_float.print_stat();;


let reset_all () =
  Arith_cache.reset_cache();
  Arith_cache.reset_stat();
  Arith_float.reset_cache();
  Arith_float.reset_stat();;


reset_all();;
Gc.compact();;
(* allocated = 79346 *)
mem_stat();;


(**************************)
(* Examples *)
let heart_poly = expr_to_vector_fun `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +
  &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 + 
  &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;

let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 - 
  #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;
let poly_ineq = (expr_to_vector_fun o rand o concl o 
		   REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;

let heart_min = `-- #1.7435` and
	poly_min = `&0`;;

let heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,
  `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
let poly_dom = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]`,
	`[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;


(***********************************)

let test_verify pp poly_tm min_flag val_tm (xx,zz) eps =
  let total_start = Sys.time() in
  let n = (get_dim o fst o dest_abs) poly_tm in
  let xx1 = convert_to_float_list pp true xx and
      zz1 = convert_to_float_list pp false zz in
  let xx_float = map float_of_float_tm (dest_list xx1) and
      zz_float = map float_of_float_tm (dest_list zz1) in
  let eval_fs, tf = mk_verification_functions pp poly_tm min_flag val_tm in
  let certificate = run_test tf xx_float zz_float false 0.0 true true true true eps in
  let c1 = transform_result xx_float zz_float certificate in
  let start = Sys.time() in
  let result = m_verify_list n pp eval_fs c1 xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Total time: %f; Verification time: %f" (finish -. total_start) (finish -. start)) in
    result;;


(******)

(* 
   PVS: 79.68; 26.14
   8 (10): 27.937; 9.176
   64 (6): 24.249; 5.672
   512 (3): 23.113; 3.428

   Why is the base 10 much faster than 8?
   Possible explanation: the domain is described by decimal numbers,
   so computations with the base 10 are faster in general (the approximation is better:
   requires less digits).
   10 (10): 23.205; 4.376
   10 (10, cached, float_cached): 20.001; 1.548
   10 (10, float_cached): 19.769; 1.744
   100 (5): 21.733; 3.180
   100 (5, cached): 20.737; 2.196
*)


reset_all();;
test_verify 10 heart_poly true heart_min heart_dom 1e-10;;

Arith_cache.print_stat();;
Arith_float.print_stat();;

(* 117589 *)
mem_stat();;

Gc.compact();;
(* 80340 *)
mem_stat();;

reset_all();;
Gc.compact();;
(* 79372 *)
mem_stat();;

(* 
   8 (10): 215.953; 112.399
   64 (6): 162.754; 62.588
   64 (5): 150.573; 49.991
   512 (3): 137.967; 32.250

   10 (10): 185.211; 83.785
   100 (5): 139.821; 40.975
   100 (5, cached): 119.267; 20.009
*)
reset_all ();;
(*
test_verify 5 poly_ineq true poly_min poly_dom 0.0;;
Arith_cache.print_stat();;
*)

(******)

let pp = 10;;
let n = (get_dim o fst o dest_abs) poly_ineq;;
let xx, zz = poly_dom;;
let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

Arith_cache.print_stat();;
Arith_float.print_stat();;

let eval_fs, tf = mk_verification_functions pp poly_ineq true poly_min;;

Arith_cache.print_stat();;
Arith_float.print_stat();;

let certificate = run_test tf xx_float zz_float false 0.0 true true true true 0.0;;
let c1 = transform_result xx_float zz_float certificate;;

reset_all();;

(* 10 (10, cached): 30.589 *)
(* 10 (10, cached, float_cached): 16.137 *)
(* 10 (10, float_cached): 17.001 *)
(* 100 (5, cached): 20.101 *)
(* 100 (5, cached, float_cached): 10.452 *)

let _ =
  let start = Sys.time() in
  let result = m_verify_list n pp eval_fs c1 xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;

Arith_cache.print_stat();;
Arith_float.print_stat();;

Gc.compact();;
(* 89346 *)
mem_stat();;

reset_all();;
Gc.compact();;
(* 79973 *)
mem_stat();;


(* num *)

let add_list = !Arith_cache.add_list and
    mul_list = !Arith_cache.mul_list and
    sub_le_list = !Arith_cache.sub_le_list;;

(* 10: 24.621 *)
(* 100: 7.612 *)
test 1 (map Arith_hash.raw_add_conv_hash) add_list;;
(* 100: 22.681 *)
test 1 (map Arith_hash.raw_mul_conv_hash) mul_list;;
(* 100: 9.917 *)
test 1 (map (fun tm1, tm2 -> Arith_hash.raw_sub_and_le_hash_conv tm1 tm2)) sub_le_list;;

Arith_cache.reset_cache();;

(* 10: 6.064 *)
(* 100: 1.884 *)
test 1 (map raw_add_conv_hash) add_list;;
(* 100: 2.396 *)
test 1 (map raw_mul_conv_hash) mul_list;;
(* 100: 2.384 *)
test 1 (map (fun tm1, tm2 -> raw_sub_and_le_hash_conv tm1 tm2)) sub_le_list;;


(****************)
(* float *)

let mul_lo_list = !Arith_float.mul_lo_list and
    mul_hi_list = !Arith_float.mul_hi_list and
    add_lo_list = !Arith_float.add_lo_list and
    add_hi_list = !Arith_float.add_hi_list;;

(* 10: 10.308 *)
reset_all();;
test 1 (map (fun p,tm1,tm2 -> float_mul_lo p tm1 tm2)) mul_lo_list;;
(* 10: 13.152 *)
reset_all();;
test 1 (map (fun p,tm1,tm2 -> float_mul_hi p tm1 tm2)) mul_hi_list;;

(* 10: 2.688 *)
reset_all();;
test 1 (map (fun p,tm1,tm2 -> float_add_lo p tm1 tm2)) add_lo_list;;
(* 10: 3.104 *)
reset_all();;
test 1 (map (fun p,tm1,tm2 -> float_add_hi p tm1 tm2)) add_hi_list;;

(***********)

let float_hash tm =
  let s, n_tm, e_tm = dest_float tm in
    s ^ (num_tm_hash n_tm) ^ "e" ^ (num_tm_hash e_tm);;


let float_op_hash pp tm1 tm2 =
  string_of_int pp ^ float_hash tm1 ^ "x" ^ float_hash tm2;;

let float_mul_table = Hashtbl.create 10000;;

let float_mul_lo_cached pp tm1 tm2 =
  let hash = float_op_hash pp tm1 tm2 in
  try
    Hashtbl.find float_mul_table hash
  with Not_found ->
    let result = float_mul_lo pp tm1 tm2 in
    let _ = Hashtbl.add float_mul_table hash result in
      result;;

reset_all();;  

(* 10: 3.624 *)
test 1 (map (fun p,tm1,tm2 -> float_mul_lo_cached p tm1 tm2)) mul_lo_list;;
(* 2150 *)
Hashtbl.length float_mul_table;;
(* 24044 *)
length mul_lo_list;;


let x = 2;;



(****************)

Hashtbl.length Arith_cache.mul_table;;
Hashtbl.length Arith_cache.sub_le_table;;
Hashtbl.length Arith_cache.add_table;;


(* 100: 0.148 *)
test 1 (map Arith_hash.raw_suc_conv_hash) !Arith_cache.suc_list;;
(* 100: 0.180 *)
test 1 (map Arith_hash.raw_eq0_hash_conv) !Arith_cache.eq0_list;;
(* 100: 0.532 *)
test 1 (map Arith_hash.raw_div_hash_conv) !Arith_cache.div_list;;

(* 100: 10.196 *)
test 1 (map (fun tm1, tm2 -> Arith_hash.raw_sub_and_le_hash_conv tm1 tm2)) !Arith_cache.sub_le_list;;




let mul_table = Hashtbl.create 100000;;

let mul_cache1 tm =
  if Hashtbl.mem mul_table tm then
    Hashtbl.find mul_table tm
  else
    let result = Arith_hash.raw_mul_conv_hash tm in
    let _ = Hashtbl.add mul_table tm result in
      result;;


(* 100: 25.882 *)
Hashtbl.clear mul_table;;
test 1 (map mul_cache1) !Arith_cache.mul_list;;
(* 100: 44.398 *)
test 1 (map mul_cache1) !Arith_cache.mul_list;;

(* 100: 22.609 *)
test 1 (map (Hashtbl.mem mul_table)) !Arith_cache.mul_list;;
(* 100: 22.233 *)
test 1 (map (Hashtbl.find mul_table)) !Arith_cache.mul_list;;
(* 100: 0.044 *)
test 1 (map Hashtbl.hash) !Arith_cache.mul_list;;

let rec num_tm_hash tm =
  if is_comb tm then
    let b_tm, n_tm = dest_comb tm in
    let str = (fst o dest_const) b_tm in
      str ^ num_tm_hash n_tm
  else
    "";;


let op_tm_hash tm =
  let lhs, tm2 = dest_comb tm in
  let tm1 = rand lhs in
    num_tm_hash tm1 ^ "x" ^ num_tm_hash tm2;;


(* 0.340 *)
test 1 (map op_tm_hash) !Arith_cache.mul_list;;
(* 0.428 *)
test 1 (map (Hashtbl.hash o op_tm_hash)) !Arith_cache.mul_list;;

(******)

let mul_table2 = Hashtbl.create 10000;;
let add_table2 = Hashtbl.create 10000;;
let div_table2 = Hashtbl.create 10000;;

let mul_cache2 tm =
  let hash = op_tm_hash tm in
    try
      Hashtbl.find mul_table2 hash
    with Not_found ->
      let result = Arith_hash.raw_mul_conv_hash tm in
      let _ = Hashtbl.add mul_table2 hash result in
	result;;

let add_cache2 tm =
  let hash = op_tm_hash tm in
    try
      Hashtbl.find add_table2 hash
    with Not_found ->
      let result = Arith_hash.raw_add_conv_hash tm in
      let _ = Hashtbl.add add_table2 hash result in
	result;;

let div_cache2 tm =
  let hash = op_tm_hash tm in
    try
      Hashtbl.find div_table2 hash
    with Not_found ->
      let result = Arith_hash.raw_div_hash_conv tm in
      let _ = Hashtbl.add div_table2 hash result in
	result;;

Hashtbl.clear div_table2;;
(* 100: 0.016 *)
test 1 (map div_cache2) !Arith_cache.div_list;;
(* 12 *)
Hashtbl.length div_table2;;
(* 100: 0.016 *)
test 1 (map div_cache2) !Arith_cache.div_list;;


Hashtbl.clear mul_table2;;
(* 100: 2.536 *)
test 1 (map mul_cache2) !Arith_cache.mul_list;;
(* 4687 *)
Hashtbl.length mul_table2;;
(* 100: 0.384 *)
test 1 (map mul_cache2) !Arith_cache.mul_list;;

Hashtbl.clear add_table2;;
(* 100: 2.052 *)
test 1 (map add_cache2) !Arith_cache.add_list;;
(* 5184 *)
Hashtbl.length add_table2;;
(* 100: 1.548 *)
test 1 (map add_cache2) !Arith_cache.add_list;;



let op_sizes tm =
  let lhs, tm2 = dest_comb tm in
  let tm1 = rand lhs in
  let list1 = striplist dest_comb tm1 and
      list2 = striplist dest_comb tm2 in
    length list1, length list2;;

let l0 = map op_sizes !Arith_cache.mul_list;;
(* 172 *)
length (List.filter (fun p -> fst p = 1) l0);;
(* 514 *)
length (List.filter (fun p -> fst p = 2) l0);;
(* 345 *)
length (List.filter (fun p -> fst p = 3) l0);;
(* 6 *)
length (List.filter (fun p -> fst p = 4) l0);;
(* 106 *)
length (List.filter (fun p -> fst p = 5) l0);;
(* 2872 *)
length (List.filter (fun p -> fst p = 6) l0);;
(* 672 *)
length (List.filter (fun p -> fst p = 7) l0);;

(* 0 *)
length (List.filter (fun p -> snd p = 1) l0);;
(* 93 *)
length (List.filter (fun p -> snd p = 2) l0);;
(* 1 *)
length (List.filter (fun p -> snd p = 3) l0);;
(* 13 *)
length (List.filter (fun p -> snd p = 4) l0);;
(* 175 *)
length (List.filter (fun p -> snd p = 5) l0);;
(* 4187 *)
length (List.filter (fun p -> snd p = 6) l0);;
(* 218 *)
length (List.filter (fun p -> snd p = 7) l0);;