# HG changeset patch # User blanchet # Date 1328288455 -3600 # Node ID 30e9720cc0b9f8db76d2ba44afebcf9b59f68ec5 # Parent 0e490b9e8422aba66417da7f4490332fa61acf69 optimization: slice caching in case two consecutive slices are nearly identical diff -r 0e490b9e8422 -r 30e9720cc0b9 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100 @@ -23,7 +23,8 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * atp_format * string * string * string))) list} + -> (real * (bool * ((int * atp_format * string * string) * string))) + list} val force_sos : bool Config.T val e_smartN : string @@ -88,10 +89,10 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * atp_format * string * string * string))) list} + -> (real * (bool * ((int * atp_format * string * string) * string))) list} (* "best_slices" must be found empirically, taking a wholistic approach since - the ATPs are run in parallel. The "real" components give the faction of the + the ATPs are run in parallel. The "real" component gives the faction of the time available given to the slice and should add up to 1.0. The "bool" component indicates whether the slice's strategy is complete; the "int", the preferred number of facts to pass; the first "string", the preferred type @@ -150,7 +151,8 @@ type T = (atp_config * stamp) Symtab.table val empty = Symtab.empty val extend = I - fun merge data : T = Symtab.merge (eq_snd op =) data + fun merge data : T = + Symtab.merge (eq_snd (op =)) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") ) @@ -246,14 +248,12 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, (500, FOF, "mono_tags??", combsN, - e_fun_weightN))), - (0.334, (true, (50, FOF, "mono_guards??", combsN, - e_fun_weightN))), - (0.333, (true, (1000, FOF, "mono_tags??", combsN, + [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))), + (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))), + (0.333, (true, ((1000, FOF, "mono_tags??", combsN), e_sym_offset_weightN)))] else - [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))] + [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))] end} val e = (eN, e_config) @@ -278,9 +278,9 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN, + [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN), sosN))), - (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN, + (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -305,7 +305,7 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN, + K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN), "")))]} val satallax = (satallaxN, satallax_config) @@ -338,17 +338,21 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN, + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN), sosN))), - (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN, + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN), sosN))), - (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN, + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} val spass = (spassN, spass_config) +val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN) +val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN) +val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN) + (* Experimental *) val spass_new_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass_new"), @@ -364,10 +368,9 @@ prem_kind = #prem_kind spass_config, best_slices = fn _ => (* FUDGE *) - [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN, - "" (* spass_incompleteN *)))), - (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))), - (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]} + [(0.300, (true, (spass_new_macro_slice_1, ""))), + (0.333, (true, (spass_new_macro_slice_2, ""))), + (0.333, (true, (spass_new_macro_slice_3, "")))]} val spass_new = (spass_newN, spass_new_config) @@ -407,15 +410,17 @@ best_slices = fn ctxt => (* FUDGE *) (if is_old_vampire_version () then - [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))), - (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))), - (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))] + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN), + sosN))), + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))), + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN), + no_sosN)))] else - [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN, + [(0.333, (false, ((150, vampire_tff0, "poly_guards??", + combs_or_liftingN), sosN))), + (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN), sosN))), - (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN, - sosN))), - (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN, + (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -438,10 +443,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))), - (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))), - (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))), - (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]} + K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))), + (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))), + (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))), + (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -457,9 +462,9 @@ conj_sym_kind = Hypothesis, prem_kind = Hypothesis, best_slices = - K [(1.0, (false, (200, format, type_enc, - if is_format_higher_order format then keep_lamsN - else combsN, "")))]} + K [(1.0, (false, ((200, format, type_enc, + if is_format_higher_order format then keep_lamsN + else combsN), "")))]} val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit) val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple" @@ -518,7 +523,7 @@ prem_kind = prem_kind, best_slices = fn ctxt => let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in - [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))] + [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))] end} fun remotify_config system_name system_versions best_slice diff -r 0e490b9e8422 -r 30e9720cc0b9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Feb 03 18:00:55 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Feb 03 18:00:55 2012 +0100 @@ -147,7 +147,7 @@ let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of SOME {best_slices, ...} => - exists (fn (_, (_, (_, format, _, _, _))) => is_format format) + exists (fn (_, (_, ((_, format, _, _), _))) => is_format format) (best_slices ctxt) | NONE => false end @@ -174,7 +174,7 @@ if is_reconstructor name then reconstructor_default_max_relevant else if is_atp thy name then - fold (Integer.max o #1 o snd o snd o snd) + fold (Integer.max o #1 o fst o snd o snd o snd) (get_slices slice (#best_slices (get_atp thy name) ctxt)) 0 else (* is_smt_prover ctxt name *) SMT_Solver.default_max_relevant ctxt name @@ -651,10 +651,10 @@ |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o snd) rths) end - fun run_slice (slice, (time_frac, (complete, - (best_max_relevant, format, best_type_enc, - best_lam_trans, extra)))) - time_left = + fun run_slice time_left (cache_key, cache_value) + (slice, (time_frac, (complete, + (key as (best_max_relevant, format, best_type_enc, + best_lam_trans), extra)))) = let val num_facts = length facts |> is_none max_relevant @@ -663,14 +663,6 @@ val type_enc = type_enc |> choose_type_enc soundness best_type_enc format val fairly_sound = is_type_enc_fairly_sound type_enc - val facts = - facts |> map untranslated_fact - |> not fairly_sound - ? filter_out (is_dangerous_prop ctxt o prop_of o snd) - |> take num_facts - |> polymorphism_of_type_enc type_enc <> Polymorphic - ? monomorphize_facts - |> map (apsnd prop_of) val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = ((real_ms time_left @@ -695,20 +687,32 @@ case lam_trans of SOME s => s | NONE => best_lam_trans - val (atp_problem, pool, fact_names, _, sym_tab) = - prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_enc false lam_trans readable_names true hyp_ts - concl_t facts + val value as (atp_problem, _, fact_names, _, _) = + if cache_key = SOME key then + cache_value + else + facts + |> map untranslated_fact + |> not fairly_sound + ? filter_out (is_dangerous_prop ctxt o prop_of o snd) + |> take num_facts + |> polymorphism_of_type_enc type_enc <> Polymorphic + ? monomorphize_facts + |> map (apsnd prop_of) + |> prepare_atp_problem ctxt format conj_sym_kind prem_kind + type_enc false lam_trans readable_names true hyp_ts + concl_t fun weights () = atp_problem_weights atp_problem val full_proof = debug orelse isar_proof - val core = + val command = File.shell_path command ^ " " ^ arguments ctxt full_proof extra slice_timeout weights ^ " " ^ File.shell_path prob_file - val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1" - val _ = atp_problem |> lines_for_atp_problem format - |> cons ("% " ^ command ^ "\n") - |> File.write_list prob_file + |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" + val _ = + atp_problem |> lines_for_atp_problem format + |> cons ("% " ^ command ^ "\n") + |> File.write_list prob_file val ((output, run_time), (atp_proof, outcome)) = TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command @@ -745,27 +749,24 @@ end | NONE => NONE) | _ => outcome - in - ((pool, fact_names, sym_tab), - (output, run_time, atp_proof, outcome)) - end + in ((SOME key, value), (output, run_time, atp_proof, outcome)) end val timer = Timer.startRealTimer () fun maybe_run_slice slice - (result as (_, (_, run_time0, _, SOME _))) = + (result as (cache, (_, run_time0, _, SOME _))) = let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in if Time.<= (time_left, Time.zeroTime) then result else - run_slice slice time_left - |> (fn (stuff, (output, run_time, atp_proof, outcome)) => - (stuff, (output, Time.+ (run_time0, run_time), + run_slice time_left cache slice + |> (fn (cache, (output, run_time, atp_proof, outcome)) => + (cache, (output, Time.+ (run_time0, run_time), atp_proof, outcome))) end | maybe_run_slice _ result = result in - ((Symtab.empty, Vector.fromList [], Symtab.empty), + ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), ("", Time.zeroTime, [], SOME InternalError)) |> fold maybe_run_slice actual_slices end @@ -781,7 +782,8 @@ () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output - val ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) = + val ((_, (_, pool, fact_names, _, sym_tab)), + (output, run_time, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = if mode = Normal andalso