1 (* ========================================================================== *)
2 (* FLYSPECK - CODE INFORMAL *)
4 (* Chapter: Nonlinear *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 (* Interactive scripts for the running of interval arithmetic code from
13 Execution done in computational_build.hl
16 (* START NONLINEAR INEQS *)
17 (* reneeds "nonlinear/ineqdata3q1h.hl";; *)
18 (* reneeds "nonlinear/strongdodec_ineq.hl";; *)
20 flyspeck_needs "leg/enclosed_def.hl";;
21 flyspeck_needs "general/sphere.hl";;
22 (* flyspeck_needs "nonlinear/ineq.hl";; *)
23 flyspeck_needs "nonlinear/main_estimate_ineq.hl";;
24 (* flyspeck_needs "nonlinear/strongdodec_ineq.hl";; *)
26 flyspeck_needs "nonlinear/lemma.hl";;
27 flyspeck_needs "nonlinear/functional_equation.hl";;
28 flyspeck_needs "nonlinear/parse_ineq.hl";;
29 flyspeck_needs "nonlinear/optimize.hl";;
30 flyspeck_needs "general/flyspeck_lib.hl";;
31 flyspeck_needs "nonlinear/auto_lib.hl";;
32 (* flyspeck_needs "../projects_discrete_geom/bcc_lattice.hl";; *)
35 module Scripts = struct
37 let idq_of_string s = hd(Ineq.getexact s);;
39 let expand_string = map (fun t->t.idv) o Ineq.getprefix;;
41 let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags;;
45 let split_sp = Str.split(Str.regexp "\n") in
46 let p = process_to_string("grep split "^flyspeck_dir
47 ^"/../interval_code/qed_log.txt "
48 ^"| sed 's/^.*ineq./\"/' "
49 ^"| sed 's/., secs.*$/\";/' "
50 ^"| sed 's/ split.*$//g' "
52 ^" | sed 's/;//g' ") in
53 Parse_ineq.nub (split_sp p);;
57 let a = filter (fun t -> List.length (get_split_tags t) > 0) !Ineq.ineqs in
58 let a' = filter (fun t -> mem t.id unfinished_cases) a in
59 map (fun t-> t.id) a';;
60 List.length hassplit;;
64 (* lists of inequality ids *)
67 Parse_ineq.nub (map (fun t -> t.idv) (!Ineq.ineqs));;
69 let finished_cases() =
70 let split_sp= Str.split (Str.regexp "\n") in
71 let p = process_to_string ("cat "^flyspeck_dir
72 ^"/../interval_code/qed_log_2012.txt "
73 (* ^"| grep 'Aug 1[67].*2013' " *)
75 ^"| sed 's/^.*ineq(/\"/' "
76 ^"| sed 's/., secs.*$/\";/' "
77 ^"| sed 's/ split(.*$//g' "
79 ^" | sed 's/;//g' ") in
80 Parse_ineq.nub (split_sp p);;
83 let unfinished_cases() = subtract (all_cases()) (finished_cases());;
86 let isdodec s = (mem Strongdodec (idq_of_string s).tags) in
87 filter isdodec (all_cases());;
90 (* *************************************************************************** *)
91 (* C++ interval verification *)
92 (* *************************************************************************** *)
96 "9563139965D"; (* derived lp, disregard it *)
99 let special_concerns = [
100 (* deprecated "2065952723 A1"; *) (* requires special code, FAILS ON THACKMAC. *)
105 (* deprecated "2065952723 A1";
106 "5556646409";"4322269127"; (* LC functions *)
107 "5512912661"; "6843920790"; "4828966562"; (* num1 *) *)
110 let testids = ref[];;
113 let view nth = idq_of_string (List.nth !testids nth);;
121 let testid = "FXZXPNS";;
122 Optimize.testsplit false testid;;
123 map (Optimize.testsplit true) !testids;;
126 (* map (Auto_lib.testsplit true) (!testids);; *)
128 let execute_interval_cases cases bool =
129 (* let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags in
130 let nonquad = filter (not o isquad) cases in *)
131 map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
133 let execute_interval_allbutdodec bool =
134 execute_interval_cases (subtract (all_cases()) (union disregard dodec_cases)) bool;;
136 let execute_interval_all bool =
137 execute_interval_cases (subtract (all_cases()) (disregard)) bool;;
139 (* execute_interval_allbutdodec true;; *)
142 (* open Optimize;; *)
144 let process_cases_testid testid =
145 let idq = idq_of_string testid in
146 let (s,tags,ineq) = Optimize.idq_fields idq in
147 let ls = Optimize.get_split_tags idq in
148 if (ls=[]) then (s,tags,ineq) else
149 let cases = Optimize.split_all_h0 [(ineq,ls)] in
150 (s^" case-",tags,List.nth cases 1);;
152 let interactive_debug_stuff testid =
153 let (id,tags,case) = process_cases_testid testid in
154 let ife b t = e(if b then t else ALL_TAC) in
155 let is_xconvert = mem Xconvert tags in
156 let is_branch = mem Branching tags in
157 let _ = g (mk_imp (`NONLIN`,case)) in
158 let _ = e(Optimize.PRELIM_REWRITE_TAC) in
159 let _ = ife (is_branch) Optimize.BRANCH_TAC in
160 let _ = ife (is_xconvert) Optimize.X_OF_Y_TAC in
161 let _ = ife (is_branch && not(is_xconvert))
162 (Optimize.SERIES3Q1H_5D_TAC) in
163 let _ = e (Optimize.STYLIZE_TAC) in
164 e (Optimize.WRAPUP_TAC);;
166 (* *************************************************************************** *)
168 (* *************************************************************************** *)
172 Parse_ineq.execute_cfsqp o idq_of_string;;
175 let us = map (idq_of_string) ts in
176 !(Parse_ineq.execute_cfsqp_list us);;
178 let execute_cfsqp() = cfsqp (all_cases());;
180 (* *************************************************************************** *)
182 (* *************************************************************************** *)
184 let rec finalize = function (* use time from most recent verification *)
186 | (x,t)::vs -> if (exists (fun (x',_) -> (x'=x)) vs) then finalize vs
187 else (x,t)::(finalize vs);;
190 let rr = map snd r in
193 let hour r = float_of_int r /. (60.0 *. 60.0);;
195 let finished_times,finished_rejects =
196 let split_sp = Str.split (Str.regexp "\n") in
197 let split_semi = Str.split (Str.regexp ";") in
198 let int_s [x;y] = try
200 with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
202 let p = process_to_string ("cat "^flyspeck_dir
203 ^"/../interval_code/qed_log_2012.txt "
204 (* ^"| grep 'Aug 1[67].*2013' " *)
205 ^"| sed 's!^//.*$!!'"
206 ^"| sed 's/^.*ineq(//' "
207 ^"| sed 's/., svn.*$//' "
208 ^" | sed 's/., *msecs.*$//' "
209 ^"| sed 's/., *cell.*$//' "
210 ^"| sed 's/., secs./;/' "
212 let (accept,rejects) = partition (fun t -> List.length t =2)
213 (map split_semi (split_sp p)) in
214 (map int_s accept,Parse_ineq.nub rejects);;
216 let finished_times_msecs,finished_rejects_msecs =
217 let split_sp = Str.split (Str.regexp "\n") in
218 let split_semi = Str.split (Str.regexp ";") in
219 let int_s [x;y] = try
221 with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
223 let p = process_to_string ("grep msecs "^flyspeck_dir
224 ^"/../interval_code/qed_log_2012.txt "
225 ^"| sed 's!^//.*$!!'"
226 ^"| sed 's/^.*ineq(//' "
227 ^"| sed 's/., *cell.*$/;/' "
228 ^"| sed 's/., secs.[0-9]*//' "
229 ^"| sed 's/., *msecs./;/' "
231 let (accept,rejects) = partition (fun t -> List.length t =2)
232 (map split_semi (split_sp p)) in
233 (map int_s accept,Parse_ineq.nub rejects);;
237 let all = all_cases() in
238 let ft = finalize finished_times in
239 let split = Str.split(Str.regexp " +split") in
240 let fti = filter (fun (x,_) -> mem (hd (split x)) all) ft in
241 sort (fun (_,y) (_,y') -> (y>y')) fti;;
243 let fast_cases = filter (fun (_,t) -> t<=5) times;;
250 hour(total(filter (fun (t,_) ->
251 Str.string_match (Str.regexp "QITNPEA 4003") t 0) times));;
253 hour (total (filter (fun (t,_) ->
254 Str.string_match (Str.regexp "ZTGIJCF23") t 0) times));;
257 (* *************************************************************************** *)
258 (* splits, test for missing cases, -- none found! may 27, 2011 *)
259 (* *************************************************************************** *)
262 let split = Str.split(Str.regexp " +split") in
263 let ss = map split ls in
264 let ss2 = filter (fun t-> List.length t = 2) ss in
265 let pair bs = (List.nth bs 0,List.nth bs 1) in
266 let nodigit = Str.split(Str.regexp "[^0-9]") in
267 let digitize s = map int_of_string (nodigit s) in
268 let f = function | b::bs -> (b,pair (unions (map digitize bs)))
269 | _ -> failwith "case_splits" in
272 let rec unify_splits = function
274 | (s,(_,t)):: _ as ys -> let (st,xs') = partition (fun (s',(_,t')) -> (s'=s & t'=t)) ys in
275 (s,Parse_ineq.nub (map (fun (_,(r',_ )) -> r') st),t) ::unify_splits xs';;
277 let case_splits_execute =
278 let vv = unify_splits (case_splits (map fst finished_times)) in
279 filter (fun (_,ls,r) -> not ((0--(r-1)) = sort (<) ls)) vv;;
283 (* *************************************************************************** *)
284 (* inventory of which inequalities actually get used in the proof *)
285 (* *************************************************************************** *)
287 let flyspeck_used_ineqs =
288 (* Merge_ineq.tsk_hyp *)
289 ["TSKAJXY-GXSABWC DIV"; "TSKAJXY-IYOUOBF sharp v2";
290 "TSKAJXY-IYOUOBF sym";
291 "TSKAJXY-RIBCYXU sharp"; "TSKAJXY-RIBCYXU sym"; "TSKAJXY-TADIAMB";
292 "TSKAJXY-WKGUESB sym"; "TSKAJXY-XLLIPLS"; "TSKAJXY-delta_x4";
295 Merge_ineq.ztg4_ineqs @
297 (* Merge_ineq.cell3_hyp *)
299 ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";
300 "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW"] @
302 (* Merge_ineq.CRKIBMP *)
304 ["GRKIBMP A V2"; "GRKIBMP B V2"] @
306 (* Mege_ineq.g_quqya_goal *)
308 ["FHBVYXZ a";"FHBVYXZ b";"FWGKMBZ"] @
310 (* Merge_ineq.gamma10_gamma11_concl *)
312 ["GLFVCVK4 2477216213";"QITNPEA 5400790175 a";"QITNPEA 5400790175 b";"FWGKMBZ"] @
314 (* Merge_ineq.gamma23_full8_x_gamma *)
318 (* Merge_ineq.cell3_008 *)
319 [ "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM"] @
321 (* Merge_ineq.gamma23_keep135_x_gamma *)
324 Merge_ineq.QITNPEA1_9063653052_hypl @
326 Merge_ineq.g_qxd_hypl @
328 Merge_ineq.gamma_qx_hypl @
331 (* (map (fun t -> t.idv) (Ineq.getprefix "OXLZLEZ 6346351218")) @ *)
334 (map (fun t -> t.idv) (filter Merge_ineq.is_ox3q1h (!Ineq.ineqs))) @
336 (* packing chapter, TSK and OXL *)
337 (map (fun t -> t.idv) Merge_ineq.packing_ineq_data) @
340 ["5735387903"; "5490182221"] @
342 (* Pent_hex.get_ineq *)
344 (map (fun t -> t.idv) (Ineq.getprefix "7550003505")) @
346 (* Parse_ineq.lpstring () : *)
348 (map (fun t -> t.idv) (Ineq.getfield Lp)) @
349 (map (fun t -> t.idv) (Ineq.getfield Lpsymmetry)) @
352 ["5584033259";"6170936724";"5691615370"] @
353 ["6170936724";"8673686234 a";"8673686234 b";"8673686234 c"] @
356 (let has_packid = (fun t -> not(intersect ["UKBRPFE";"WAZLDCD";"BIEFJHU"] (Ineq.flypaper_ids t) = [])) in
357 let idl = (filter has_packid !Ineq.ineqs) in
358 (map (fun t -> t.idv) idl)) @
361 (* Terminal, Pent_hex :
362 grep get_main_nonlinear local/*.hl | sed 's/^.*get_main_nonlinear//g' | sed 's/").*$/";/g' *)
412 "OMKYNLT 3336871894";
413 "OMKYNLT 3336871894";
452 "4680581274 delta top issue";
454 "4680581274 delta issue";
456 "7697147739 delta top issue";
458 "7697147739 delta issue";
465 let all_ineqs = map (fun t -> t.idv) (!Ineq.ineqs);;
466 let remain_to_be_used = Flyspeck_lib.nub (sort (<) (subtract all_ineqs flyspeck_used_ineqs));;
474 (* generate file prep.hl of all preprocessed inequalities. *)
476 (* edit "#" -> " #" in printer.ml to defuse "--#0.02" bug *)
477 (* needs "printer.ml";; *)
479 module Preprocess = struct
482 (* let add_inequality _ = ();; *)
484 let ineq = Sphere.ineq;;
485 let print_tag t = match t with
486 | Branching -> "Branching"
488 | Disallow_derivatives -> "Disallow_derivatives"
489 | Onlycheckderiv1negative -> "Onlycheckderiv1negative"
490 | Dim_red -> "Dim_red"
491 | Dim_red_backsym -> "Dim_red_backsym"
492 | Quad_cluster f -> "Quad_cluster "^(string_of_float f)
493 | Set_rad2 -> "Set_rad2"
494 | Delta126min f -> "Delta126min "^(string_of_float f)
495 | Delta126max f -> "Delta126max "^(string_of_float f)
496 | Widthcutoff f -> "Widthcutoff "^(string_of_float f)
497 | Delta135min f -> "Delta135min "^(string_of_float f)
498 | Delta135max f -> "Delta126max "^(string_of_float f)
502 let print_one (s,tgl,ii) =
503 let p = Printf.sprintf in
504 let tgs = filter (fun s -> not(s="")) (map print_tag tgl) in
505 let jsemi = Flyspeck_lib.unsplit ";" (fun x-> x) in
506 let tl = jsemi tgs in
507 let is = print_to_string pp_print_qterm (Sphere.all_forall ii) in
508 Flyspeck_lib.join_lines [
518 let prep = (Optimize.preprocess_split_idq
519 (hd (Ineq.getexact (s)))) in
521 Flyspeck_lib.join_lines (map print_one prep) in
523 ((s,map (fun (s,_,_) -> s) prep),v);;
525 (* return the association list of idv -> list of new idv *)
526 let preprocess filename =
527 let cc = subtract (all_cases()) (disregard) in
528 let header = "(* Auto generated file of preprocessed inequalities. See Scripts.exec *)\n\n" in
529 let h1 = "(* "^flyspeck_version()^"\n "^build_date() ^"*)\n\n" in
530 let h2 = "(* need to defuse --# in printer.ml *)\n\n" in
531 let h3 = "module Prep = struct\n\n"^
532 "let prep_ineqs = ref ([]:ineq_datum list);;\n\n "^
533 "let add_inequality i = \n"^
534 "let _ = prep_ineqs:= i :: !prep_ineqs in\n"^
536 let p = map preprocess1 cc in
537 let v = Flyspeck_lib.join_lines (map snd p) in
538 let e = "\n\nend;;" in
539 let _ = Flyspeck_lib.output_filestring filename (header^h1^h2^h3^v^e) in
542 let prep_file = Filename.temp_file "prep" ".hl";;
544 let exec()= preprocess prep_file;;
545 (* exec();; needs prep_file;; *)