# HG changeset patch # User blanchet # Date 1321459574 -3600 # Node ID 0cd6e59bd0b5fd7069877ae3f65abe56f4c2b7cc # Parent 2b1dde0b1c309d9dfefadb8b3e59bac9f5c95850 give each time slice its own lambda translation diff -r 2b1dde0b1c30 -r 0cd6e59bd0b5 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Nov 16 16:35:19 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Nov 16 17:06:14 2011 +0100 @@ -23,7 +23,7 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * atp_format * string * string))) list} + -> (real * (bool * (int * atp_format * string * string * string))) list} val force_sos : bool Config.T val e_smartN : string @@ -56,7 +56,8 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind - -> (Proof.context -> int * atp_format * string) -> string * atp_config + -> (Proof.context -> int * atp_format * string * string) + -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -70,6 +71,7 @@ open ATP_Problem open ATP_Proof +open ATP_Translate (* ATP configuration *) @@ -85,15 +87,16 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * atp_format * 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 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 - system (which should be sound or quasi-sound); the second "string", extra - information to the prover (e.g., SOS or no SOS). + system (which should be sound or quasi-sound); the second "string", the + preferred lambda translation scheme; the third "string", 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 @@ -242,11 +245,14 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))), - (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))), - (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))] + [(0.333, (true, (500, FOF, "mono_tags??", combinatorsN, + e_fun_weightN))), + (0.334, (true, (50, FOF, "mono_guards??", combinatorsN, + e_fun_weightN))), + (0.333, (true, (1000, FOF, "mono_tags??", combinatorsN, + e_sym_offset_weightN)))] else - [(1.0, (true, (500, FOF, "mono_tags??", method)))] + [(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))] end} val e = (eN, e_config) @@ -271,8 +277,10 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))), - (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))] + [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN, + sosN))), + (0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN, + no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -296,7 +304,8 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]} + K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN, + "")))]} val satallax = (satallaxN, satallax_config) @@ -326,9 +335,12 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", sosN))), - (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", sosN))), - (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", no_sosN)))] + [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN, + sosN))), + (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN, + sosN))), + (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN, + no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -345,9 +357,12 @@ prem_kind = #prem_kind spass_config, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*, - (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))), - (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)] + [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN, + sosN))) (*, + (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN, + sosN))), + (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN, + no_sosN)))*)] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -389,13 +404,16 @@ best_slices = fn ctxt => (* FUDGE *) (if is_old_vampire_version () then - [(0.333, (false, (150, FOF, "poly_guards??", sosN))), - (0.333, (false, (500, FOF, "mono_tags??", sosN))), - (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))] + [(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))), + (0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))), + (0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))] else - [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))), - (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))), - (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))]) + [(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN, + sosN))), + (0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN, + sosN))), + (0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN, + no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -417,10 +435,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))), - (0.25, (false, (125, z3_tff0, "mono_simple", ""))), - (0.125, (false, (62, z3_tff0, "mono_simple", ""))), - (0.125, (false, (31, z3_tff0, "mono_simple", "")))]} + K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))), + (0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))), + (0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))), + (0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -435,7 +453,10 @@ known_failures = known_szs_status_failures, conj_sym_kind = Hypothesis, prem_kind = Hypothesis, - best_slices = K [(1.0, (false, (200, format, type_enc, "")))]} + best_slices = + K [(1.0, (false, (200, format, type_enc, + if is_format_higher_order format then keep_lamsN + else combinatorsN, "")))]} val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit) val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple" @@ -493,8 +514,8 @@ conj_sym_kind = conj_sym_kind, prem_kind = prem_kind, best_slices = fn ctxt => - let val (max_relevant, format, type_enc) = best_slice ctxt in - [(1.0, (false, (max_relevant, format, type_enc, "")))] + let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in + [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))] end} fun remotify_config system_name system_versions best_slice @@ -516,42 +537,43 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K (750, FOF, "mono_tags??") (* FUDGE *)) + (K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *)) + (K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *)) + (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] - (K (250, FOF, "mono_guards??") (* FUDGE *)) + (K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *)) val remote_z3_tptp = remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, z3_tff0, "mono_simple") (* FUDGE *)) + (K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom - Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *)) + Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *)) val remote_iprover = remote_atp iproverN "iProver" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??") (* FUDGE *)) + (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *)) val remote_iprover_eq = remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??") (* FUDGE *)) + (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] - [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, explicit_tff0, "mono_simple") (* FUDGE *)) + [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis + (K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom - Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *)) + Hypothesis + (K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] - [("#START OF PROOF", "Proved Goals:")] - [(OutOfResources, "Too many function symbols"), - (Crashed, "Unrecoverable Segmentation Fault")] - Hypothesis Hypothesis - (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *)) + [("#START OF PROOF", "Proved Goals:")] + [(OutOfResources, "Too many function symbols"), + (Crashed, "Unrecoverable Segmentation Fault")] + Hypothesis Hypothesis + (K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *)) (* Setup *) diff -r 2b1dde0b1c30 -r 0cd6e59bd0b5 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 16:35:19 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 17:06:14 2011 +0100 @@ -15,6 +15,7 @@ val type_has_top_sort : typ -> bool val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic + val metis_lam_transs : string list val parse_metis_options : (string list option * string option) parser val setup : theory -> theory end @@ -253,10 +254,10 @@ (schem_facts @ ths)) end -val lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] +val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] fun consider_opt s = - if member (op =) lam_transs s then apsnd (K (SOME s)) + if member (op =) metis_lam_transs s then apsnd (K (SOME s)) else apfst (K (SOME [s])) val parse_metis_options = diff -r 2b1dde0b1c30 -r 0cd6e59bd0b5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 16:35:19 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 17:06:14 2011 +0100 @@ -120,6 +120,7 @@ open ATP_Systems open ATP_Translate open ATP_Reconstruct +open Metis_Tactic open Sledgehammer_Util open Sledgehammer_Filter @@ -161,7 +162,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 @@ -419,7 +420,7 @@ in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor (Metis (type_enc, lam_trans)) = - Metis_Tactic.metis_tac [type_enc] lam_trans + metis_tac [type_enc] lam_trans | tac_for_reconstructor SMT = SMT_Solver.smt_tac fun timed_reconstructor reconstr debug timeout ths = @@ -637,7 +638,7 @@ end fun run_slice (slice, (time_frac, (complete, (best_max_relevant, format, best_type_enc, - extra)))) + best_lam_trans, extra)))) time_left = let val num_facts = @@ -678,9 +679,7 @@ val lam_trans = case lam_trans of SOME s => s - | NONE => - if is_type_enc_higher_order type_enc then keep_lamsN - else combinatorsN (* FIXME ### improve *) + | NONE => best_lam_trans val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, _, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind @@ -789,7 +788,10 @@ let val used_facts = used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof - val reconstrs = standard_reconstructors lam_trans + val reconstrs = + standard_reconstructors + (if member (op =) metis_lam_transs lam_trans then lam_trans + else combinatorsN) in (used_facts, fn () => @@ -1024,8 +1026,7 @@ preplay = K play, message = fn play => let - val (_, override_params (* FIXME ###: use these *)) = - extract_reconstructor reconstr + val (_, override_params) = extract_reconstructor reconstr val one_line_params = (play, proof_banner mode name, used_facts, minimize_command override_params name, subgoal,