(* ========================================================================== *) (* 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;;