formal_lp/hypermap/verify_all.hl

   1 needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;
   2
   3 module Verify_all = struct
   4
   5 open List;;
   6 open Flyspeck_lp;;
   7 open Lp_certificate;;
   8
   9 let cert_dir = ref (flyspeck_dir ^ "/../formal_lp/glpk/binary");;
  10
  11 let get_files_with_prefix dir prefix =
  12   let files = Array.to_list (Sys.readdir dir) in
  13   let n = String.length prefix in
  14   let files1 = filter (fun f -> String.length f >= n) files in
  15   let files2 = filter (fun f -> String.sub f 0 n = prefix) files1 in
  16     map (fun f -> sprintf "%s/%s" dir f) files2;;
  17
  18 let get_certificate_files_with_prefix dir prefix =
  19   let alt_dir = dir ^ "/lp_certificates" in
  20   let files1 = get_files_with_prefix dir prefix in
  21   let files2 =
  22     if Sys.file_exists alt_dir then
  23       get_files_with_prefix alt_dir prefix
  24     else
  25       [] in
  26     files1 @ files2;;
  27
  28 let mem_stat () =
  29   let stat = Gc.stat() in
  30   let word = float_of_int (Sys.word_size / 8) in
  31   let free = float_of_int stat.Gc.free_words *. word /. 1024.0 in
  32   let total = float_of_int stat.Gc.heap_words *. word /. 1024.0 in
  33   let allocated = total -. free in
  34   let str = sprintf "allocated = %f (free = %f; total_size = %f; %f)\n"
  35     allocated free total (free /. total) in
  36     print_string str;;
  37
  38
  39 let verify_file =
  40   let counter = ref 0 and
  41       total = ref 0 in
  42   let report s =
  43     Format.print_string s; Format.print_newline(); Format.print_flush() in
  44   let process certificate =
  45     let _ = counter := !counter + 1 in
  46     let _ = report (sprintf "%d/%d" !counter !total) in
  47       verify_lp_certificate certificate in
  48   let process_all file =
  49     let certificates = read_lp_certificates file in
  50     let _ = counter := 0 in
  51     let _ = total := length certificates in
  52     let start = Unix.gettimeofday() in
  53     let result = map process certificates in
  54     let finish = Unix.gettimeofday() in
  55       result, finish -. start in
  56     fun file ->
  57       let _ = report (sprintf "Verifying %s" file) in
  58       let result, time = process_all file in
  59       let _ = Gc.compact() in
  60       let _ = mem_stat() in
  61         result, time;;
  62
  63
  64 let init_ineqs() =
  65   try
  66     let _ = Lp_ineqs.find_ineq false 3 "y1_def" in
  67     let _ = report "Inequalities are already initialized" in
  68       ()
  69   with Not_found ->
  70     Flyspeck_lp.init_ineqs();;
  71
  72
  73
  74 let verify_easy() =
  75   let _ = init_ineqs() in
  76   let files = get_certificate_files_with_prefix !cert_dir "easy" in
  77     map verify_file files;;
  78
  79 let verify_hard() =
  80   let _ = init_ineqs() in
  81   let files = get_certificate_files_with_prefix !cert_dir "hard" in
  82     map verify_file files;;
  83
  84 let verify_all() =
  85   let result_hard = verify_hard() in
  86   let result_easy = verify_easy() in
  87     result_hard @ result_easy;;
  88
  89 let test_result result =
  90   let ths = List.flatten (map fst result) in
  91   let time = map snd result in
  92   let total = end_itlist (+.) time in
  93   let concls = setify (map concl ths) in
  94   let hyps = unions (map (fun th -> filter (fun tm -> not (is_binary "iso" tm)) (hyp th)) ths) in
  95     total, concls, hyps;;
  96
  97
  98
  99 end;;