# HG changeset patch # User blanchet # Date 1305206958 -7200 # Node ID c1909691bbf09a46786e5aa96203b7ed69783656 # Parent 626e292d22a7288a8accc2c5882d6515a963cf46 allow each slice to have its own type system diff -r 626e292d22a7 -r c1909691bbf0 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu May 12 15:29:18 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 12 15:29:18 2011 +0200 @@ -22,8 +22,7 @@ conj_sym_kind : formula_kind, prem_kind : formula_kind, formats : format list, - best_slices : Proof.context -> (real * (bool * int)) list, - best_type_systems : string list} + best_slices : Proof.context -> (real * (bool * (int * string list))) list} val e_weight_method : string Config.T val e_default_fun_weight : real Config.T @@ -43,7 +42,7 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind -> format list - -> (Proof.context -> int) -> string list -> string * atp_config + -> (Proof.context -> int * string list) -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -71,13 +70,19 @@ conj_sym_kind : formula_kind, prem_kind : formula_kind, formats : format list, - best_slices : Proof.context -> (real * (bool * int)) list, - best_type_systems : string list} + best_slices : Proof.context -> (real * (bool * (int * string list))) list} -(* "best_slices" and "best_type_systems" must be found empirically, taking a - wholistic approach since the ATPs are run in parallel. "best_type_systems" - should be of the form [sound] or [unsound, sound], where "sound" is a sound - type system and "unsound" is an unsound one. *) +(* "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; these 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 "string list", the preferred type + systems, which should be of the form [sound] or [unsound, sound], where + "sound" is a sound type system and "unsound" is an unsound one. + + 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 for + remote provers and if slicing is disabled. *) val known_perl_failures = [(CantConnect, "HTTP error"), @@ -212,13 +217,13 @@ prem_kind = Conjecture, formats = [Fof], best_slices = fn ctxt => + (* FUDGE *) if effective_e_weight_method ctxt = e_slicesN then - [(0.33333, (true, 100 (* FUDGE *))) (* sym_offset_weight *), - (0.33333, (true, 1000 (* FUDGE *))) (* auto *), - (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)] + [(0.333, (true, (100, ["mangled_preds?"]))) (* sym_offset_weight *), + (0.333, (true, (1000, ["mangled_preds?"]))) (* auto *), + (0.334, (true, (200, ["mangled_preds?"]))) (* fun_weight *)] else - [(1.0, (true, 250 (* FUDGE *)))], - best_type_systems = ["mangled_preds?"]} + [(1.0, (true, (250, ["mangled_preds?"])))]} val e = (eN, e_config) @@ -248,9 +253,9 @@ prem_kind = Conjecture, formats = [Fof], best_slices = - K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *), - (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)], - best_type_systems = ["mangled_preds"]} + (* FUDGE *) + K [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *), + (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]} val spass = (spassN, spass_config) @@ -285,9 +290,9 @@ prem_kind = Conjecture, formats = [Fof], best_slices = - K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *), - (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)], - best_type_systems = ["mangled_tags!", "mangled_preds?"]} + (* FUDGE *) + K [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *), + (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]} val vampire = (vampireN, vampire_config) @@ -309,8 +314,9 @@ conj_sym_kind = Hypothesis, prem_kind = Hypothesis, formats = [Fof], - best_slices = K [(1.0, (false, 250 (* FUDGE *)))], - best_type_systems = [] (* FIXME *)} + best_slices = + (* FUDGE (FIXME) *) + K [(1.0, (false, (250, [])))]} val z3_atp = (z3_atpN, z3_atp_config) @@ -348,8 +354,7 @@ val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_max_relevant - best_type_systems : atp_config = + conj_sym_kind prem_kind formats best_slice : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn _ => fn timeout => fn _ => @@ -364,24 +369,20 @@ conj_sym_kind = conj_sym_kind, prem_kind = prem_kind, formats = formats, - best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))], - best_type_systems = best_type_systems} - -fun int_average f xs = fold (Integer.add o f) xs 0 div length xs + best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]} fun remotify_config system_name system_versions ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, - best_slices, best_type_systems, ...} : atp_config) : atp_config = + best_slices, ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures conj_sym_kind prem_kind formats - (int_average (snd o snd) o best_slices) best_type_systems + (best_slices #> List.last #> snd #> snd) fun remote_atp name system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_max_relevant best_type_systems = + conj_sym_kind prem_kind formats best_slice = (remote_prefix ^ name, remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_max_relevant - best_type_systems) + conj_sym_kind prem_kind formats best_slice) fun remotify_atp (name, config) system_name system_versions = (remote_prefix ^ name, remotify_config system_name system_versions config) @@ -390,14 +391,14 @@ val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] val remote_tofof_e = remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"] + Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *)) val remote_sine_e = remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof] - (K 500 (* FUDGE *)) ["args", "preds", "tags"] + (K (500, ["poly_args"]) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Conjecture - [Tff, Fof] (K 250 (* FUDGE *)) ["simple"] + [Tff, Fof] (K (250, ["simple_types"]) (* FUDGE *)) (* Setup *) diff -r 626e292d22a7 -r c1909691bbf0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:18 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:18 2011 +0200 @@ -135,7 +135,7 @@ if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else - fold (Integer.max o snd o snd o snd) + fold (Integer.max o fst o snd o snd o snd) (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0 end @@ -346,7 +346,8 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Polymorphic, Const_Arg_Types), Simple_Types All_Types] + [Preds (Polymorphic, Const_Arg_Types), + Preds (Mangled_Monomorphic, Nonmonotonic_Types)] fun adjust_dumb_type_sys formats (Simple_Types level) = if member (op =) formats Tff then (Tff, Simple_Types level) @@ -362,8 +363,7 @@ fun run_atp auto name ({exec, required_execs, arguments, proof_delims, known_failures, - conj_sym_kind, prem_kind, formats, best_slices, best_type_systems, - ...} : atp_config) + conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) ({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...} : params) @@ -371,8 +371,6 @@ let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val (format, type_sys) = - determine_format_and_type_sys best_type_systems formats type_sys val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name @@ -430,13 +428,15 @@ |> filter_out (curry (op =) ~1 o fst) |> map (Untranslated_Fact o apfst (fst o nth facts)) end - fun run_slice blacklist - (slice, (time_frac, (complete, default_max_relevant))) + fun run_slice blacklist (slice, (time_frac, (complete, + (best_max_relevant, best_type_systems)))) time_left = let val num_facts = length facts |> is_none max_relevant - ? Integer.min default_max_relevant + ? Integer.min best_max_relevant + val (format, type_sys) = + determine_format_and_type_sys best_type_systems formats type_sys val fairly_sound = is_type_sys_fairly_sound type_sys val facts = facts |> not fairly_sound @@ -521,11 +521,11 @@ | _ => outcome in ((pool, conjecture_shape, facts_offset, fact_names), - (output, msecs, atp_proof, outcome)) + (output, msecs, type_sys, atp_proof, outcome)) end val timer = Timer.startRealTimer () fun maybe_run_slice blacklist slice - (result as (_, (_, msecs0, _, SOME _))) = + (result as (_, (_, msecs0, _, _, SOME _))) = let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in @@ -533,14 +533,16 @@ result else (run_slice blacklist slice time_left - |> (fn (stuff, (output, msecs, atp_proof, outcome)) => - (stuff, (output, int_opt_add msecs0 msecs, atp_proof, - outcome)))) + |> (fn (stuff, (output, msecs, type_sys, atp_proof, + outcome)) => + (stuff, (output, int_opt_add msecs0 msecs, type_sys, + atp_proof, outcome)))) end | maybe_run_slice _ _ result = result fun maybe_blacklist_facts_and_retry iter blacklist (result as ((_, _, facts_offset, fact_names), - (_, _, atp_proof, SOME (UnsoundProof false)))) = + (_, _, type_sys, atp_proof, + SOME (UnsoundProof false)))) = (case used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof of [] => result @@ -554,7 +556,8 @@ | maybe_blacklist_facts_and_retry _ _ result = result in ((Symtab.empty, [], 0, Vector.fromList []), - ("", SOME 0, [], SOME InternalError)) + ("", SOME 0, hd fallback_best_type_systems, [], + SOME InternalError)) |> fold (maybe_run_slice []) actual_slices (* The ATP found an unsound proof? Automatically try again without the offending facts! *) @@ -567,13 +570,13 @@ the proof file too. *) fun cleanup prob_file = if dest_dir = "" then try File.rm prob_file else NONE - fun export prob_file (_, (output, _, _, _)) = + fun export prob_file (_, (output, _, _, _, _)) = if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((pool, conjecture_shape, facts_offset, fact_names), - (output, msecs, atp_proof, outcome)) = + (output, msecs, type_sys, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = if not auto andalso