formal_lp/glpk/test_hard.hl

   1 needs "../formal_lp/glpk/build_certificates.hl";;
   2
   3 open List;;
   4 open Glpk_link;;
   5 open Lpproc;;
   6 open Lp_certificate;;
   7 open Lp_informal_computations;;
   8 open Build_certificates;;
   9 open Hard_lp;;
  10
  11 let hard_bbs = hard_bb();;
  12
  13 test_mode := false;;
  14
  15 test_mode := true;;
  16 print_progress := true;;
  17
  18 let bb = nth hard_bbs 8;;
  19 map length (faces bb);;
  20 let cert = build_certificate true bb;;
  21 certificate_info cert;;
  22 build_test_split cert.root_case;;
  23
  24 write_lp_certificates (sprintf "%s/hard8.dat" !output_dir) [cert];;
  25 certificate_info cert;;
  26 build_test_split cert.root_case;;
  27
  28
  29
  30 let rec correct bb cert =
  31   match cert with
  32     | Lp_terminal _ -> cert
  33     | Lp_split (info, cs) ->
  34         (match info.split_type with
  35            | "add_big" ->
  36                let opp xs = nub (xs @ map (C opposite_edge bb) xs) in
  37                let long_edge = opp bb.d_edge_225_252 in
  38                let long_edge_faces = zip (map (C face_of_dart bb) long_edge) long_edge in
  39                let dart = assoc info.split_face long_edge_faces in
  40                let cases = map (correct bb) cs in
  41                  Lp_split ({info with split_face = dart}, cases)
  42            | "edge" ->
  43                let bb1 = modify_bb bb false ["e_225_252", info.split_face] [] in
  44                let cases = map2 correct [bb1; bb] cs in
  45                  Lp_split (info, cases)
  46            | _ ->
  47                let cases = map (correct bb) cs in
  48                  Lp_split (info, cases));;
  49
  50
  51
  52 let rec get_infos name = function
  53   | Lp_terminal _ -> []
  54   | Lp_split (info, cs) ->
  55       let list = flatten (map (get_infos name) cs) in
  56         if info.split_type = name then info :: list else list;;
  57
  58
  59 let c = hd (read_lp_certificates (sprintf "%s/hard1.dat" !output_dir));;
  60 certificate_info c;;
  61 build_test_split c.root_case;;
  62 let add_big1 = get_infos "add_big" c.root_case;;
  63
  64 let bb = nth hard_bbs 0;;
  65 let c2_root = correct bb c.root_case;;
  66 let c2 = {c with root_case = c2_root};;
  67
  68 certificate_info c;;
  69 certificate_info c2;;
  70
  71 build_test_split c2.root_case;;
  72 let add_big2 = get_infos "add_big" c2.root_case;;
  73
  74 write_lp_certificates (sprintf "%s/hard0.dat" !output_dir) [c2];;
  75
  76 let c =