1 (* ========================================================================== *)
4 (* Linear Programming, AMPL format (non-formal) *)
5 (* Chapter:Tame Hypermap *)
6 (* Lemma: KCBLRQC (Tame Table B) *)
7 (* Author: Thomas C. Hales *)
9 (* ========================================================================== *)
13 The model considers nodes of type (p,q,0) and computes
16 It also computes the constant a(5,0,1).
20 flyspeck_needs "strictbuild.hl";;
21 flyspeck_needs "../glpk/glpk_link.ml";;
22 flyspeck_needs "../graph_generator/graph_control.hl";;
24 module Tame_table = struct
26 let squander_target = Graph_control.flyspeck_properties.Graph_control.squander_target;;
27 let table_weight_d = Graph_control.flyspeck_properties.Graph_control.table_weight_d;;
28 let table_weight_a = Graph_control.flyspeck_properties.Graph_control.table_weight_a;;
29 let table_weight_b = Graph_control.flyspeck_properties.Graph_control.table_weight_b;;
30 let node_card_max_at_exceptional_vertex = Graph_control.flyspeck_properties.Graph_control.node_card_max_at_exceptional_vertex;;
31 let fl x = float_of_int x /. 10000.0;;
33 type lptype = Lp_unset
37 let string_of_lptype t = match t with
38 | Lp_infeasible -> "infeasible"
40 | Lp_value u -> Printf.sprintf "%3.3f" u;;
42 let rec cart b c = match b with
44 |b::bs -> (map (fun t -> (b,t)) c) @ cart bs c;;
51 let sprintf = Printf.sprintf;;
53 let glpk_dir = flyspeck_dir ^ "/../glpk";;
56 let model = glpk_dir^ "/minorlp/tame_table.mod";;
57 let tmpfile = "/tmp/tame_table.dat";;
58 let dumpfile = "/tmp/tmp.out";;
62 mutable lpvalue : lptype;
68 (* the initial configuration always has a quarter at 0 *)
77 let string_of_node t =
78 Printf.sprintf "%d %d %d %s" t.p t.q t.r (string_of_lptype t.lpvalue);;
80 let ampl_of_nt outs nt =
83 pr"param p := %d;" nt.p;
84 pr"param q := %d;" nt.q;
85 pr"param r := %d;\n" nt.r;
87 Printf.fprintf outs "%s" j;;
90 let nt = mk_node 3 3 0 in
91 display_ampl tmpfile ampl_of_nt nt;;
93 (* running of branch in glpsol *)
95 let set_lpvalue nt (f,r) = (* side effects *)
97 if (List.length f > 0) then nt.lpvalue <- Lp_infeasible
98 else if (List.length r = 1) then nt.lpvalue <- Lp_value (float_of_string(hd r))
99 else nt.lpvalue <- Lp_unset in
102 let init_lpvalue nt =
103 let _ = match nt.lpvalue with
104 | Lp_unset -> (set_lpvalue nt (solve_branch_f model dumpfile "tausum" ampl_of_nt nt))
106 let _ = report (string_of_node nt) in
109 (* display_ampl tmpfile ampl_of_nt (mk_node 5 0 0);; *)
111 let fpqr ((p,q),r) = init_lpvalue (mk_node p q r);;
113 let fpq (p,q) = fpqr((p,q),0);;
115 (* solve_branch_f model dumpfile "tausum" ampl_of_nt (mk_node 3 4 0);; *)
117 (* Each exception region contributes at least tame_table_d_5 *)
120 let target_ub = 1.542 in
121 let _ = target_ub > fl squander_target or failwith "bad target value" in
122 let tame_table_d_5 = 0.4818 in
123 let _ = tame_table_d_5 < fl (List.nth table_weight_d 5) or failwith "bad d5 value" in
124 filter (fun t -> match t.lpvalue with
125 Lp_infeasible -> false
127 | Lp_value s -> (s +. float_of_int t.r *. tame_table_d_5 < target_ub));;
129 let graph_control_unfound_b (t:node_type ) = match (t.lpvalue) with
132 let eps = 1.0e-10 in (* allow roundoff error *)
133 let (_,_,v) = List.find (fun (a,b,_) -> (a=t.p && b = t.q)) table_weight_b in
136 with Not_found -> true)
140 let filter2 = filter graph_control_unfound_b;;
142 (* The case (p,q,r) = (0,2,0) is rejected by the convexity hypothesis. *)
143 (* The case (p,q,r) = (5,0,0) is done with calculation 4652969746 *)
145 let known_exceptions (t:node_type) =
146 not((t.p = 0 && t.q = 2 && t.r = 0) or (t.p = 5 && t.q = 0 && t.r = 0));;
148 let filter3 = filter known_exceptions;;
150 let tame_table_lp_data() = (map fpq (cart (0--10) (0--10)));;
152 let tame_table_b_info() =
153 let n = filter3 (filter2 (filter1 (tame_table_lp_data()))) in
154 if (List.length n = 0) then "All b table values have been accounted for in informal lp tests (ignoring 0,2,0 and 5,0,0)"
155 else "Unaccounted for b values: \n" ^ join_lines (map string_of_node n);;
157 (* If r >= 4, then the dihedral sum is greater than 2 Pi *)
160 let a = (cart (cart (0--6) (0--6)) (1--3)) in
161 filter (fun ((p,q),r) -> (p+q+r=6)) a;;
164 let badvalues_a (t:node_type) = match (t.lpvalue) with
167 let eps = 1.0e-10 in (* allow roundoff error *)
168 let (_,v) = List.find (fun (a,_) -> (a=t.p && (6-a) = t.q + t.r)) table_weight_a in
171 with Not_found -> true)
175 let filter_a = filter badvalues_a;;
177 let tame_table_a_info() =
178 let n = filter_a (filter1 (map fpqr pqrvalues )) in
179 if (List.length n = 0) then "All a table values have been accounted for in informal lp tests"
180 else "Unaccounted for a values: \n" ^ join_lines (map string_of_node n);;
183 let s = join_lines [tame_table_b_info();tame_table_a_info()] in