# HG changeset patch # User blanchet # Date 1309175567 -7200 # Node ID b342cd12553343739edf4055375397c3f24ad29c # Parent 3e4889375781c3ba5319380c01e57a65c116bef3 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway diff -r 3e4889375781 -r b342cd125533 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 27 13:52:47 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 27 13:52:47 2011 +0200 @@ -8,7 +8,6 @@ val proverK = "prover" val prover_timeoutK = "prover_timeout" val keepK = "keep" -val full_typesK = "full_types" val type_sysK = "type_sys" val slicingK = "slicing" val e_weight_methodK = "e_weight_method" @@ -630,8 +629,6 @@ end fun invoke args = - let - val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK - in Mirabelle.register (init, sledgehammer_action args, done) end + Mirabelle.register (init, sledgehammer_action args, done) end diff -r 3e4889375781 -r b342cd125533 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 13:52:47 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 13:52:47 2011 +0200 @@ -23,7 +23,7 @@ prem_kind : formula_kind, formats : format list, best_slices : - Proof.context -> (real * (bool * (int * string list * string))) list} + Proof.context -> (real * (bool * (int * string * string))) list} val e_smartN : string val e_autoN : string @@ -52,7 +52,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) -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -81,19 +81,19 @@ prem_kind : formula_kind, formats : format list, best_slices : - Proof.context -> (real * (bool * (int * string list * string))) list} + Proof.context -> (real * (bool * (int * 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; these should add up to 1.0. The "bool" + 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 "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. + preferred number of facts to pass; the first "string", the preferred type + system; the second "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 for - remote provers and if slicing is disabled. *) + time available if the other slices fail early and also because it is used if + slicing is disabled (e.g., by the minimizer). *) val known_perl_failures = [(CantConnect, "HTTP error"), @@ -217,11 +217,11 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))), - (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))), - (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))] + [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))), + (0.334, (true, (50, "mangled_preds?", e_fun_weightN))), + (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))] else - [(1.0, (true, (500, ["mangled_tags?"], method)))] + [(1.0, (true, (500, "mangled_tags?", method)))] end} val e = (eN, e_config) @@ -237,7 +237,7 @@ val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], - arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ => + arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout)) |> sos = sosN ? prefix "-SOS=1 ", @@ -256,9 +256,9 @@ formats = [FOF], best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, ["mangled_tags"], sosN))), - (0.333, (false, (300, ["poly_tags?"], sosN))), - (0.334, (true, (50, ["mangled_tags?"], no_sosN)))] + [(0.333, (false, (150, "mangled_tags", sosN))), + (0.333, (false, (300, "poly_tags?", sosN))), + (0.334, (true, (50, "mangled_tags?", no_sosN)))] |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -273,7 +273,7 @@ val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], - arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ => + arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^ " --thanks \"Andrei and Krystof\" --input_file" |> sos = sosN ? prefix "--sos on ", @@ -297,9 +297,9 @@ formats = [FOF], best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, ["poly_preds"], sosN))), - (0.334, (true, (50, ["mangled_preds?"], no_sosN))), - (0.333, (false, (500, ["mangled_tags?"], sosN)))] + [(0.333, (false, (150, "poly_preds", sosN))), + (0.334, (true, (50, "mangled_preds?", no_sosN))), + (0.333, (false, (500, "mangled_tags?", sosN)))] |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -325,7 +325,7 @@ formats = [FOF], best_slices = (* FUDGE (FIXME) *) - K [(1.0, (false, (250, [], "")))]} + K [(1.0, (false, (250, "mangled_preds?", "")))]} val z3_atp = (z3_atpN, z3_atp_config) @@ -385,8 +385,8 @@ prem_kind = prem_kind, formats = formats, best_slices = fn ctxt => - let val (max_relevant, type_syss) = best_slice ctxt in - [(1.0, (false, (max_relevant, type_syss, "")))] + let val (max_relevant, type_sys) = best_slice ctxt in + [(1.0, (false, (max_relevant, type_sys, "")))] end} fun remotify_config system_name system_versions best_slice @@ -406,36 +406,35 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K (750, ["mangled_tags?"]) (* FUDGE *)) + (K (750, "mangled_tags?") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] - (K (200, ["mangled_preds?"]) (* FUDGE *)) + (K (200, "mangled_preds?") (* FUDGE *)) val remote_z3_atp = - remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *)) + remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *)) val remote_leo2 = remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF] - (K (100, ["simple"]) (* FUDGE *)) + (K (100, "simple") (* FUDGE *)) val remote_satallax = remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF] - (K (64, ["simple"]) (* FUDGE *)) + (K (64, "simple") (* FUDGE *)) val remote_sine_e = - remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) - Axiom Conjecture [FOF] - (K (500, ["mangled_preds?"]) (* FUDGE *)) + remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom + Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - [TFF, FOF] (K (100, ["simple"]) (* FUDGE *)) + [TFF, FOF] (K (100, "simple") (* FUDGE *)) val remote_tofof_e = remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *)) + Axiom Hypothesis [TFF] (K (150, "simple") (* 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 [CNF_UEQ] - (K (50, ["mangled_tags?"]) (* FUDGE *)) + (K (50, "mangled_tags?") (* FUDGE *)) (* Setup *) diff -r 3e4889375781 -r b342cd125533 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 13:52:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 13:52:47 2011 +0200 @@ -12,7 +12,6 @@ val auto : bool Unsynchronized.ref val provers : string Unsynchronized.ref val timeout : int Unsynchronized.ref - val full_types : bool Unsynchronized.ref val default_params : Proof.context -> (string * string) list -> params val setup : theory -> theory end; @@ -65,7 +64,6 @@ val provers = Unsynchronized.ref "" val timeout = Unsynchronized.ref 30 -val full_types = Unsynchronized.ref false val _ = ProofGeneralPgip.add_preference Preferences.category_proof @@ -79,11 +77,6 @@ "Sledgehammer: Time Limit" "ATPs will be interrupted after this time (in seconds)") -val _ = - ProofGeneralPgip.add_preference Preferences.category_proof - (Preferences.bool_pref full_types - "Sledgehammer: Full Types" "ATPs will use full type information") - type raw_param = string * string list val default_default_params = @@ -108,16 +101,15 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("non_blocking", "blocking"), - ("partial_types", "full_types"), ("no_isar_proof", "isar_proof"), ("no_slicing", "slicing")] val params_for_minimize = - ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters", + ["debug", "verbose", "overlord", "type_sys", "max_mono_iters", "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"] -val property_dependent_params = ["provers", "full_types", "timeout"] +val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse @@ -218,7 +210,6 @@ [("provers", [case !provers of "" => default_provers_param_value ctxt | s => s]), - ("full_types", [if !full_types then "true" else "false"]), ("timeout", let val timeout = !timeout in [if timeout <= 0 then "none" else string_of_int timeout] @@ -272,10 +263,10 @@ |> mode = Auto_Try ? single o hd val type_sys = if mode = Auto_Try then - Smart_Type_Sys true + NONE else case lookup_string "type_sys" of - "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types") - | s => Dumb_Type_Sys (type_sys_from_string s) + "smart" => NONE + | s => SOME (type_sys_from_string s) val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_option lookup_int "max_relevant" val max_mono_iters = lookup_int "max_mono_iters" diff -r 3e4889375781 -r b342cd125533 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 13:52:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 13:52:47 2011 +0200 @@ -18,17 +18,13 @@ datatype mode = Auto_Try | Try | Normal | Minimize - datatype rich_type_sys = - Dumb_Type_Sys of type_sys | - Smart_Type_Sys of bool - type params = {debug: bool, verbose: bool, overlord: bool, blocking: bool, provers: string list, - type_sys: rich_type_sys, + type_sys: type_sys option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -286,17 +282,13 @@ (** problems, results, ATPs, etc. **) -datatype rich_type_sys = - Dumb_Type_Sys of type_sys | - Smart_Type_Sys of bool - type params = {debug: bool, verbose: bool, overlord: bool, blocking: bool, provers: string list, - type_sys: rich_type_sys, + type_sys: type_sys option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -510,16 +502,11 @@ them each time. *) val atp_important_message_keep_quotient = 10 -val fallback_best_type_syss = - [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)] - -fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = - choose_format formats type_sys - | choose_format_and_type_sys best_type_syss formats - (Smart_Type_Sys full_types) = - map type_sys_from_string best_type_syss @ fallback_best_type_syss - |> find_first (if full_types then is_type_sys_virtually_sound else K true) - |> the |> choose_format formats +fun choose_format_and_type_sys best_type_sys formats type_sys_opt = + (case type_sys_opt of + SOME ts => ts + | NONE => type_sys_from_string best_type_sys) + |> choose_format formats val metis_minimize_max_time = seconds 2.0 @@ -609,14 +596,14 @@ |> maps (fn (name, rths) => map (pair name o snd) rths) end fun run_slice (slice, (time_frac, (complete, - (best_max_relevant, best_type_syss, extra)))) + (best_max_relevant, best_type_sys, extra)))) time_left = let val num_facts = length facts |> is_none max_relevant ? Integer.min best_max_relevant val (format, type_sys) = - choose_format_and_type_sys best_type_syss formats type_sys + choose_format_and_type_sys best_type_sys formats type_sys val fairly_sound = is_type_sys_fairly_sound type_sys val facts = facts |> map untranslated_fact diff -r 3e4889375781 -r b342cd125533 src/HOL/ex/atp_export.ML --- a/src/HOL/ex/atp_export.ML Mon Jun 27 13:52:47 2011 +0200 +++ b/src/HOL/ex/atp_export.ML Mon Jun 27 13:52:47 2011 +0200 @@ -120,7 +120,7 @@ " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ File.shell_path prob_file in - TimeLimit.timeLimit (seconds 0.15) bash_output command + TimeLimit.timeLimit (seconds 0.3) bash_output command |> fst |> extract_tstplike_proof_and_outcome false true proof_delims known_failures @@ -129,7 +129,7 @@ handle TimeLimit.TimeOut => SOME TimedOut val likely_tautology_prefixes = - [@{theory HOL}, @{theory Meson}, @{theory Metis}] + [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |> map (fact_name_of o Context.theory_name) fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =