1 needs "../formal_lp/glpk/build_certificates.hl";;
7 open Lp_informal_computations;;
8 open Build_certificates;;
11 let hard_bbs = hard_bb();;
16 print_progress := true;;
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;;
24 write_lp_certificates (sprintf "%s/hard8.dat" !output_dir) [cert];;
25 certificate_info cert;;
26 build_test_split cert.root_case;;
30 let rec correct bb cert =
32 | Lp_terminal _ -> cert
33 | Lp_split (info, cs) ->
34 (match info.split_type with
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)
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)
47 let cases = map (correct bb) cs in
48 Lp_split (info, cases));;
52 let rec get_infos name = function
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;;
59 let c = hd (read_lp_certificates (sprintf "%s/hard1.dat" !output_dir));;
61 build_test_split c.root_case;;
62 let add_big1 = get_infos "add_big" c.root_case;;
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};;
71 build_test_split c2.root_case;;
72 let add_big2 = get_infos "add_big" c2.root_case;;
74 write_lp_certificates (sprintf "%s/hard0.dat" !output_dir) [c2];;