# HG changeset patch # User blanchet # Date 1359651245 -3600 # Node ID 62b992e53eb81ae6d47b5840527b5be9f99fd8f3 # Parent afd0213a3dab67a49d04ef4bd13fe4ea0ffea5eb store fact filter along with ATP slice diff -r afd0213a3dab -r 62b992e53eb8 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 31 17:54:05 2013 +0100 @@ -12,7 +12,7 @@ type formula_role = ATP_Problem.formula_role type failure = ATP_Proof.failure - type slice_spec = int * atp_format * string * string * bool + type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : string list * string list, arguments : @@ -91,7 +91,7 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 200 (* FUDGE *) -type slice_spec = int * atp_format * string * string * bool +type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : string list * string list, @@ -107,18 +107,26 @@ best_max_new_mono_instances : int} (* "best_slices" must be found empirically, taking a wholistic approach since - 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 "int" - component indicates the preferred number of facts to pass; the first - "string", the preferred type system (which should be sound or quasi-sound); - the second "string", the preferred lambda translation scheme; the "bool", - whether uncurried aliased should be generated; the third "string", extra - information to the prover (e.g., SOS or no SOS). + the ATPs are run in parallel. Each slice has the format + + (time_frac, ((max_facts, fact_filter), format, type_enc, + lam_trans, uncurried_aliases), extra) + + where + + time_frac = faction of the time available given to the slice (which should + add up to 1.0) + + extra = extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the time available if the other slices fail early and also because it is used if slicing is disabled (e.g., by the minimizer). *) +val mepoN = "mepo" +val mashN = "mash" +val meshN = "mesh" + val known_perl_failures = [(CantConnect, "HTTP error"), (NoPerl, "env: perl"), @@ -209,7 +217,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, ((100, alt_ergo_tff1, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -328,11 +336,14 @@ let val heuristic = effective_e_selection_heuristic ctxt in (* FUDGE *) if heuristic = e_smartN then - [(0.333, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN)), - (0.334, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN)), - (0.333, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN))] + [(0.1667, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)), + (0.1667, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)), + (0.1666, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)), + (0.1667, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)), + (0.1667, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)), + (0.1666, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))] else - [(1.0, ((500, FOF, "mono_tags??", combsN, false), heuristic))] + [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -351,8 +362,7 @@ prem_role = Conjecture, best_slices = (* FUDGE *) - K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")), - (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))], + K [(1.0, (((1000, ""), FOF, "poly_guards??", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -390,7 +400,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, ((150, FOF, "mono_guards??", liftingN, false), ""))], + K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -434,7 +444,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)} @@ -456,7 +466,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)} @@ -497,14 +507,14 @@ prem_role = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.1667, ((150, DFG Monomorphic, "mono_native", combsN, true), "")), - (0.1667, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), - (0.1666, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), - (0.1000, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), - (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), - (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), - (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), - (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] + [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), + (0.1667, (((500, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), + (0.1666, (((50, mashN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), + (0.1000, (((250, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), + (0.1000, (((1000, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), + (0.1000, (((150, mashN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), + (0.1000, (((300, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), + (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] |> (case Config.get ctxt spass_extra_options of "" => I | opts => map (apsnd (apsnd (K opts)))), @@ -551,13 +561,16 @@ best_slices = fn ctxt => (* FUDGE *) (if is_vampire_beyond_1_8 () then - [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)), - (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)), - (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))] + [(0.1667, (((128, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), e_fun_weightN)), + (0.1667, (((128, mashN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), e_sym_offset_weightN)), + (0.1666, (((91, mepoN), vampire_tff0, "mono_native", combsN, false), e_autoN)), + (0.1667, (((64, mashN), vampire_tff0, "mono_tags??", liftingN, false), e_fun_weightN)), + (0.1667, (((1000, meshN), vampire_tff0, "poly_guards??", combs_or_liftingN, false), e_sym_offset_weightN)), + (0.1666, (((256, mepoN), vampire_tff0, "mono_native", combs_or_liftingN, false), e_fun_weightN))] else - [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)), - (0.333, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN)), - (0.334, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))]) + [(0.333, (((150, mepoN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)), + (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)), + (0.334, (((50, mashN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I), best_max_mono_iters = default_max_mono_iters, @@ -580,10 +593,10 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, ((250, z3_tff0, "mono_native", combsN, false), "")), - (0.25, ((125, z3_tff0, "mono_native", combsN, false), "")), - (0.125, ((62, z3_tff0, "mono_native", combsN, false), "")), - (0.125, ((31, z3_tff0, "mono_native", combsN, false), ""))], + K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")), + (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")), + (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")), + (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -599,7 +612,7 @@ known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = - K [(1.0, ((200, format, type_enc, + K [(1.0, (((200, ""), format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, @@ -692,32 +705,32 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *)) + (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" [] - (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) + (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_iprover_eq = remotify_atp iprover_eq "iProver-Eq" [] - (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) + (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) + (K (((100, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.3", "2.2", "2"] - (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K (((100, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"] - (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *)) + (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture - (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) + (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis - (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) + (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis - (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) + (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] @@ -725,7 +738,7 @@ (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] Hypothesis - (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *)) + (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *)) (* Setup *) diff -r afd0213a3dab -r 62b992e53eb8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 @@ -196,7 +196,7 @@ if is_reconstructor name then reconstructor_default_max_facts else if is_atp thy name then - fold (Integer.max o #1 o fst o snd o snd) + fold (Integer.max o fst o #1 o fst 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 @@ -710,8 +710,9 @@ end fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, - (key as (best_max_facts, format, best_type_enc, - best_lam_trans, best_uncurried_aliases), + (key as ((best_max_facts, best_fact_filter), format, + best_type_enc, best_lam_trans, + best_uncurried_aliases), extra))) = let val num_facts =