formal_lp/glpk/build_main.hl

   1 #load "unix.cma";;\r
   2 \r
   3 (* \r
   4 Unix.putenv "FLYSPECK_DIR" "/mnt/Repository/text_formalization";; \r
   5 *)\r
   6 \r
   7 (* The FLYSPECK_DIR environment variable must be set *)\r
   8 let flyspeck_dir = \r
   9   try Sys.getenv "FLYSPECK_DIR" with Not_found -> failwith "FLYSPECK_DIR must be set";;\r
  10 \r
  11 let hollight_dir =\r
  12   (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;\r
  13         \r
  14 let add_to_load_path path =\r
  15   if mem path !load_path then ()\r
  16   else load_path := path :: !load_path;;\r
  17 \r
  18 add_to_load_path flyspeck_dir;;\r
  19 \r
  20 (* From strictbuild.hl (required by flyspeck_lib.hl) *)\r
  21 let process_to_string unixstring =\r
  22   let p = Unix.open_process_in unixstring\r
  23   and b = Buffer.create 64 in\r
  24   let rec read () = Buffer.add_channel b p 1; read () in\r
  25     try read () with End_of_file -> (let _ = Unix.close_process_in p in Buffer.contents b);;\r
  26 \r
  27 needs "general/lib.hl";;\r
  28 needs "general/flyspeck_lib.hl";;\r
  29 \r
  30 needs "../glpk/tame_archive/lpproc.ml";;\r
  31 needs "../glpk/sphere.ml";;\r
  32 needs "../glpk/tame_archive/hard_lp.ml";;\r
  33 \r
  34 needs "../formal_lp/glpk/build_certificates.hl";;\r
  35 \r
  36 module Lp_build_main = struct\r
  37 \r
  38 open List;;\r
  39 open Lpproc;;\r
  40 open Hard_lp;;\r
  41 open Build_certificates;;\r
  42 \r
  43 type lp_bbs = {\r
  44   (* All easy lp's *)\r
  45   easy : branchnbound list;\r
  46   (* Hard lp's *)\r
  47   hard : branchnbound list;\r
  48 };;\r
  49 \r
  50 let get_lp_bbs () =\r
  51   let tame = Glpk_link.strip_archive (!archiveraw) in\r
  52   let all_bbs = map mk_bb tame in\r
  53   let hard_bbs, easy_bbs = partition (fun bb -> mem bb.hypermap_id Lpproc.hardid) all_bbs in\r
  54     {easy = easy_bbs; hard = map resolve_with_hints_include_flat hard_bbs};;\r
  55 \r
  56 \r
  57 let build_all_easy max =\r
  58   let _ = make_models false in\r
  59   let bbs = get_lp_bbs() in\r
  60   let _ = report "Building easy lp certificates" in\r
  61     build_and_save_all "easy" max true bbs.easy;;\r
  62 \r
  63 \r
  64 let build_all_hard max =\r
  65   let _ = make_models false in\r
  66   let bbs = get_lp_bbs() in\r
  67   let _ = report "Building hard lp certificates" in\r
  68     build_and_save_all "hard" max true bbs.hard;;\r
  69 \r
  70 \r
  71 let build_all max =\r
  72   let _ = build_all_easy max in\r
  73     (* Save each hard lp certificate in a separate file: max = 1 *)\r
  74   let _ = build_all_hard 1 in\r
  75     ();;\r
  76 \r
  77 \r
  78 end;;\r
  79 \r
  80 \r
  81 (*\r
  82 open Build_certificates;;\r
  83 open Lp_build_main;;\r
  84 open Hard_lp;;\r
  85 make_models false;;\r
  86 let bbs = get_lp_bbs();;\r
  87 \r
  88 let bb = List.nth bbs.hard 1;;\r
  89 test_mode := true;;\r
  90 \r
  91 let cert = build_certificate true bb;;\r
  92 Lp_certificate.certificate_info cert;;\r
  93 \r
  94 allpass_hint_include_flat 20000 [bb];;\r
  95 *)\r