(* ========================================================================== *)
(* FLYSPECK - CODE INFORMAL *)
(* *)
(* Chapter: Nonlinear *)
(* Author: Thomas C. Hales *)
(* Date: 2012-04-15 *)
(* ========================================================================== *)
(* Interactive scripts for the running of interval arithmetic code from
ineq.hl,
Execution done in computational_build.hl
*)
(* START NONLINEAR INEQS *)
(* reneeds "nonlinear/ineqdata3q1h.hl";; *)
(* reneeds "nonlinear/strongdodec_ineq.hl";; *)
flyspeck_needs "leg/enclosed_def.hl";;
flyspeck_needs "general/sphere.hl";;
(* flyspeck_needs "nonlinear/ineq.hl";; *)
flyspeck_needs "nonlinear/main_estimate_ineq.hl";;
(* flyspeck_needs "nonlinear/strongdodec_ineq.hl";; *)
flyspeck_needs "nonlinear/lemma.hl";;
flyspeck_needs "nonlinear/functional_equation.hl";;
flyspeck_needs "nonlinear/parse_ineq.hl";;
flyspeck_needs "nonlinear/optimize.hl";;
flyspeck_needs "general/flyspeck_lib.hl";;
flyspeck_needs "nonlinear/auto_lib.hl";;
(* flyspeck_needs "../projects_discrete_geom/bcc_lattice.hl";; *)
module Scripts = struct
let idq_of_string s = hd(Ineq.getexact s);;
let expand_string = map (fun t->t.idv) o Ineq.getprefix;;
let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags;;
(*
let finished_splits =
let split_sp = Str.split(Str.regexp "\n") in
let p = process_to_string("grep split "^flyspeck_dir
^"/../interval_code/qed_log.txt "
^"| sed 's/^.*ineq./\"/' "
^"| sed 's/., secs.*$/\";/' "
^"| sed 's/ split.*$//g' "
^"| sed 's/\"//g' "
^" | sed 's/;//g' ") in
Parse_ineq.nub (split_sp p);;
let hassplit =
let a = filter (fun t -> List.length (get_split_tags t) > 0) !Ineq.ineqs in
let a' = filter (fun t -> mem t.id unfinished_cases) a in
map (fun t-> t.id) a';;
List.length hassplit;;
*)
(* lists of inequality ids *)
let all_cases() =
Parse_ineq.nub (map (fun t -> t.idv) (!Ineq.ineqs));;
let finished_cases() =
let split_sp= Str.split (Str.regexp "\n") in
let p = process_to_string ("cat "^flyspeck_dir
^"/../interval_code/qed_log_2012.txt "
(* ^"| grep 'Aug 1[67].*2013' " *)
^"| sed 's!^//.*$!!'"
^"| sed 's/^.*ineq(/\"/' "
^"| sed 's/., secs.*$/\";/' "
^"| sed 's/ split(.*$//g' "
^"| sed 's/\"//g' "
^" | sed 's/;//g' ") in
Parse_ineq.nub (split_sp p);;
let unfinished_cases() = subtract (all_cases()) (finished_cases());;
let dodec_cases =
let isdodec s = (mem Strongdodec (idq_of_string s).tags) in
filter isdodec (all_cases());;
(* *************************************************************************** *)
(* C++ interval verification *)
(* *************************************************************************** *)
let disregard =
[
"9563139965D"; (* derived lp, disregard it *)
] ;;
let special_concerns = [
(* deprecated "2065952723 A1"; *) (* requires special code, FAILS ON THACKMAC. *)
];;
let nocompile =
[
(* deprecated "2065952723 A1";
"5556646409";"4322269127"; (* LC functions *)
"5512912661"; "6843920790"; "4828966562"; (* num1 *) *)
] @ disregard;;
let testids = ref[];;
(*
let view nth = idq_of_string (List.nth !testids nth);;
idq_fields(view 0);;
view 1;;
*)
(* running one id *)
(*
let testid = "FXZXPNS";;
Optimize.testsplit false testid;;
map (Optimize.testsplit true) !testids;;
*)
(* map (Auto_lib.testsplit true) (!testids);; *)
let execute_interval_cases cases bool =
(* let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags in
let nonquad = filter (not o isquad) cases in *)
map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
let execute_interval_allbutdodec bool =
execute_interval_cases (subtract (all_cases()) (union disregard dodec_cases)) bool;;
let execute_interval_all bool =
execute_interval_cases (subtract (all_cases()) (disregard)) bool;;
(* execute_interval_allbutdodec true;; *)
(* goal *)
(* open Optimize;; *)
let process_cases_testid testid =
let idq = idq_of_string testid in
let (s,tags,ineq) = Optimize.idq_fields idq in
let ls = Optimize.get_split_tags idq in
if (ls=[]) then (s,tags,ineq) else
let cases = Optimize.split_all_h0 [(ineq,ls)] in
(s^" case-",tags,List.nth cases 1);;
let interactive_debug_stuff testid =
let (id,tags,case) = process_cases_testid testid in
let ife b t = e(if b then t else ALL_TAC) in
let is_xconvert = mem Xconvert tags in
let is_branch = mem Branching tags in
let _ = g (mk_imp (`NONLIN`,case)) in
let _ = e(Optimize.PRELIM_REWRITE_TAC) in
let _ = ife (is_branch) Optimize.BRANCH_TAC in
let _ = ife (is_xconvert) Optimize.X_OF_Y_TAC in
let _ = ife (is_branch && not(is_xconvert))
(Optimize.SERIES3Q1H_5D_TAC) in
let _ = e (Optimize.STYLIZE_TAC) in
e (Optimize.WRAPUP_TAC);;
(* *************************************************************************** *)
(* TESTING CFSQP *)
(* *************************************************************************** *)
let one_cfsqp =
Parse_ineq.execute_cfsqp o idq_of_string;;
let cfsqp ts =
let us = map (idq_of_string) ts in
!(Parse_ineq.execute_cfsqp_list us);;
let execute_cfsqp() = cfsqp (all_cases());;
(* *************************************************************************** *)
(* Timing *)
(* *************************************************************************** *)
let rec finalize = function (* use time from most recent verification *)
| [] -> []
| (x,t)::vs -> if (exists (fun (x',_) -> (x'=x)) vs) then finalize vs
else (x,t)::(finalize vs);;
let total r =
let rr = map snd r in
end_itlist (+) rr;;
let hour r = float_of_int r /. (60.0 *. 60.0);;
let finished_times,finished_rejects =
let split_sp = Str.split (Str.regexp "\n") in
let split_semi = Str.split (Str.regexp ";") in
let int_s [x;y] = try
(x,int_of_string y)
with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
in
let p = process_to_string ("cat "^flyspeck_dir
^"/../interval_code/qed_log_2012.txt "
(* ^"| grep 'Aug 1[67].*2013' " *)
^"| sed 's!^//.*$!!'"
^"| sed 's/^.*ineq(//' "
^"| sed 's/., svn.*$//' "
^" | sed 's/., *msecs.*$//' "
^"| sed 's/., *cell.*$//' "
^"| sed 's/., secs./;/' "
) in
let (accept,rejects) = partition (fun t -> List.length t =2)
(map split_semi (split_sp p)) in
(map int_s accept,Parse_ineq.nub rejects);;
let finished_times_msecs,finished_rejects_msecs =
let split_sp = Str.split (Str.regexp "\n") in
let split_semi = Str.split (Str.regexp ";") in
let int_s [x;y] = try
(x,int_of_string y)
with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
in
let p = process_to_string ("grep msecs "^flyspeck_dir
^"/../interval_code/qed_log_2012.txt "
^"| sed 's!^//.*$!!'"
^"| sed 's/^.*ineq(//' "
^"| sed 's/., *cell.*$/;/' "
^"| sed 's/., secs.[0-9]*//' "
^"| sed 's/., *msecs./;/' "
) in
let (accept,rejects) = partition (fun t -> List.length t =2)
(map split_semi (split_sp p)) in
(map int_s accept,Parse_ineq.nub rejects);;
let times =
let all = all_cases() in
let ft = finalize finished_times in
let split = Str.split(Str.regexp " +split") in
let fti = filter (fun (x,_) -> mem (hd (split x)) all) ft in
sort (fun (_,y) (_,y') -> (y>y')) fti;;
let fast_cases = filter (fun (_,t) -> t<=5) times;;
(*
hour (total times);;
hour(total(filter (fun (t,_) ->
Str.string_match (Str.regexp "QITNPEA 4003") t 0) times));;
hour (total (filter (fun (t,_) ->
Str.string_match (Str.regexp "ZTGIJCF23") t 0) times));;
*)
(* *************************************************************************** *)
(* splits, test for missing cases, -- none found! may 27, 2011 *)
(* *************************************************************************** *)
let case_splits ls =
let split = Str.split(Str.regexp " +split") in
let ss = map split ls in
let ss2 = filter (fun t-> List.length t = 2) ss in
let pair bs = (List.nth bs 0,List.nth bs 1) in
let nodigit = Str.split(Str.regexp "[^0-9]") in
let digitize s = map int_of_string (nodigit s) in
let f = function | b::bs -> (b,pair (unions (map digitize bs)))
| _ -> failwith "case_splits" in
map f ss2;;
let rec unify_splits = function
| [] -> []
| (s,(_,t)):: _ as ys -> let (st,xs') = partition (fun (s',(_,t')) -> (s'=s & t'=t)) ys in
(s,Parse_ineq.nub (map (fun (_,(r',_ )) -> r') st),t) ::unify_splits xs';;
let case_splits_execute =
let vv = unify_splits (case_splits (map fst finished_times)) in
filter (fun (_,ls,r) -> not ((0--(r-1)) = sort (<) ls)) vv;;
(* *************************************************************************** *)
(* inventory of which inequalities actually get used in the proof *)
(* *************************************************************************** *)
let flyspeck_used_ineqs =
(* Merge_ineq.tsk_hyp *)
["TSKAJXY-GXSABWC DIV"; "TSKAJXY-IYOUOBF sharp v2";
"TSKAJXY-IYOUOBF sym";
"TSKAJXY-RIBCYXU sharp"; "TSKAJXY-RIBCYXU sym"; "TSKAJXY-TADIAMB";
"TSKAJXY-WKGUESB sym"; "TSKAJXY-XLLIPLS"; "TSKAJXY-delta_x4";
"TSKAJXY-eulerA"] @
Merge_ineq.ztg4_ineqs @
(* Merge_ineq.cell3_hyp *)
["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";
"QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW"] @
(* Merge_ineq.CRKIBMP *)
["GRKIBMP A V2"; "GRKIBMP B V2"] @
(* Mege_ineq.g_quqya_goal *)
["FHBVYXZ a";"FHBVYXZ b";"FWGKMBZ"] @
(* Merge_ineq.gamma10_gamma11_concl *)
["GLFVCVK4 2477216213";"QITNPEA 5400790175 a";"QITNPEA 5400790175 b";"FWGKMBZ"] @
(* Merge_ineq.gamma23_full8_x_gamma *)
["GRKIBMP A V2"] @
(* Merge_ineq.cell3_008 *)
[ "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM"] @
(* Merge_ineq.gamma23_keep135_x_gamma *)
["GRKIBMP A V2"] @
Merge_ineq.QITNPEA1_9063653052_hypl @
Merge_ineq.g_qxd_hypl @
Merge_ineq.gamma_qx_hypl @
(* Merge_ineq.ox *)
(* (map (fun t -> t.idv) (Ineq.getprefix "OXLZLEZ 6346351218")) @ *)
(* Merge_ineq: *)
(map (fun t -> t.idv) (filter Merge_ineq.is_ox3q1h (!Ineq.ineqs))) @
(* packing chapter, TSK and OXL *)
(map (fun t -> t.idv) Merge_ineq.packing_ineq_data) @
(* TameGeneral *)
["5735387903"; "5490182221"] @
(* Pent_hex.get_ineq *)
(map (fun t -> t.idv) (Ineq.getprefix "7550003505")) @
(* Parse_ineq.lpstring () : *)
(map (fun t -> t.idv) (Ineq.getfield Lp)) @
(map (fun t -> t.idv) (Ineq.getfield Lpsymmetry)) @
(* Lp_details *)
["5584033259";"6170936724";"5691615370"] @
["6170936724";"8673686234 a";"8673686234 b";"8673686234 c"] @
(* Yssqoy *)
(let has_packid = (fun t -> not(intersect ["UKBRPFE";"WAZLDCD";"BIEFJHU"] (Ineq.flypaper_ids t) = [])) in
let idl = (filter has_packid !Ineq.ineqs) in
(map (fun t -> t.idv) idl)) @
(* Terminal, Pent_hex :
grep get_main_nonlinear local/*.hl | sed 's/^.*get_main_nonlinear//g' | sed 's/").*$/";/g' *)
[ "7439076204";
"7439076204";
"7439076204";
"1834976363";
"4828966562";
"6843920790";
"1117202051";
"1117202051";
"4559601669";
"4559601669";
"4559601669b";
"4559601669b";
"4821120729";
"6459846571";
"2485876245a";
"7175074394";
"6789182745";
"4887115291";
"2125338128";
"2314572187";
"7796879304";
"1347067436";
"6601228004";
"3078028960";
"3078028960";
"3078028960";
"5546286427";
"3665919985";
"3665919985";
"7903347843";
"7997589055";
"2565248885";
"2320951108";
"5429238960";
"1948775510";
"3665919985";
"5708641738";
"1008824382";
"1586903463";
"8875146520";
"6877738680";
"9692636487";
"2485876245b";
"6762190381";
"8346775862";
"8631418063";
"8631418063";
"4821120729";
"5202826650 a";
"OMKYNLT 3336871894";
"OMKYNLT 3336871894";
"4010906068";
"4010906068";
"6833979866";
"5541487347";
"4528012043";
"7459553847";
"4143829594";
"1080462150";
"9816718044";
"3106201101";
"2200527225";
"2900061606";
"7097350062a";
"OMKYNLT 1 2";
"7645170609";
"OMKYNLT 2 1";
"7881254908";
"5026777310a";
"7720405539";
"2739661360";
"4922521904";
"2468307358";
"2739661360";
"3603097872";
"3603097872";
"3603097872";
"3603097872";
"5405130650";
"5766053833";
"5691615370";
"9563139965 d";
"9563139965 d";
"9563139965 f";
"9563139965 f";
"9563139965 e";
"9563139965 e";
"9563139965 e";
"9563139965 e";
"4680581274 delta top issue";
"4559601669";
"4680581274 delta issue";
"4680581274 a";
"7697147739 delta top issue";
"4559601669";
"7697147739 delta issue";
"7697147739 a";
"5405130650";
"3603097872";
"9096461391";
"2445657182"];;
let all_ineqs = map (fun t -> t.idv) (!Ineq.ineqs);;
let remain_to_be_used = Flyspeck_lib.nub (sort (<) (subtract all_ineqs flyspeck_used_ineqs));;
end;;
(* October, 2012 *)
(* generate file prep.hl of all preprocessed inequalities. *)
(* edit "#" -> " #" in printer.ml to defuse "--#0.02" bug *)
(* needs "printer.ml";; *)
module Preprocess = struct
open Scripts;;
(* let add_inequality _ = ();; *)
let ineq = Sphere.ineq;;
let print_tag t = match t with
| Branching -> "Branching"
| Sharp -> "Sharp"
| Disallow_derivatives -> "Disallow_derivatives"
| Onlycheckderiv1negative -> "Onlycheckderiv1negative"
| Dim_red -> "Dim_red"
| Dim_red_backsym -> "Dim_red_backsym"
| Quad_cluster f -> "Quad_cluster "^(string_of_float f)
| Set_rad2 -> "Set_rad2"
| Delta126min f -> "Delta126min "^(string_of_float f)
| Delta126max f -> "Delta126max "^(string_of_float f)
| Widthcutoff f -> "Widthcutoff "^(string_of_float f)
| Delta135min f -> "Delta135min "^(string_of_float f)
| Delta135max f -> "Delta126max "^(string_of_float f)
| _ -> ""
;;
let print_one (s,tgl,ii) =
let p = Printf.sprintf in
let tgs = filter (fun s -> not(s="")) (map print_tag tgl) in
let jsemi = Flyspeck_lib.unsplit ";" (fun x-> x) in
let tl = jsemi tgs in
let is = print_to_string pp_print_qterm (Sphere.all_forall ii) in
Flyspeck_lib.join_lines [
"add_inequality { ";
p " idv= \"%s\";" s;
" doc=\"\";";
p " tags= [%s];" tl;
p " ineq= %s;" is;
p "};;\n\n";
];;
let preprocess1 s =
let prep = (Optimize.preprocess_split_idq
(hd (Ineq.getexact (s)))) in
let v =
Flyspeck_lib.join_lines (map print_one prep) in
let _ = report v in
((s,map (fun (s,_,_) -> s) prep),v);;
(* return the association list of idv -> list of new idv *)
let preprocess filename =
let cc = subtract (all_cases()) (disregard) in
let header = "(* Auto generated file of preprocessed inequalities. See Scripts.exec *)\n\n" in
let h1 = "(* "^flyspeck_version()^"\n "^build_date() ^"*)\n\n" in
let h2 = "(* need to defuse --# in printer.ml *)\n\n" in
let h3 = "module Prep = struct\n\n"^
"let prep_ineqs = ref ([]:ineq_datum list);;\n\n "^
"let add_inequality i = \n"^
"let _ = prep_ineqs:= i :: !prep_ineqs in\n"^
" ();;\n\n" in
let p = map preprocess1 cc in
let v = Flyspeck_lib.join_lines (map snd p) in
let e = "\n\nend;;" in
let _ = Flyspeck_lib.output_filestring filename (header^h1^h2^h3^v^e) in
map fst p;;
let prep_file = Filename.temp_file "prep" ".hl";;
let exec()= preprocess prep_file;;
(* exec();; needs prep_file;; *)
end;;