# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 325c8fd0d7620f7f16859db57dc221a6b47a6f51 # Parent e5420161d11d9a4f5b54e659b7e892dea256c4dc more consolidation of MaSh code diff -r e5420161d11d -r 325c8fd0d762 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -46,15 +46,21 @@ | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident +fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN + | atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN + | atp_for_format (DFG Polymorphic) = spass_polyN + | atp_for_format (DFG Monomorphic) = spassN + | atp_for_format (TFF (Polymorphic, _)) = alt_ergoN + | atp_for_format (TFF (Monomorphic, _)) = vampireN + | atp_for_format FOF = eN + | atp_for_format CNF_UEQ = waldmeisterN + | atp_for_format CNF = eN + fun run_some_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") - val atp = - case format of - DFG Polymorphic => spass_polyN - | DFG Monomorphic => spassN - | _ => eN + val atp = atp_for_format format val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp @@ -107,13 +113,14 @@ handle TYPE _ => @{prop True} end -fun all_non_tautological_facts_of thy css_table = +fun all_non_tautological_facts_of ctxt prover thy css_table = Sledgehammer_Fact.all_facts_of thy css_table - |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology orf + |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology ctxt prover orf Sledgehammer_Filter_MaSh.is_too_meta) o snd) fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let + val atp = atp_for_format format val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val type_enc = type_enc |> type_enc_from_string Strict @@ -121,7 +128,7 @@ val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = all_non_tautological_facts_of thy css_table + val facts = all_non_tautological_facts_of ctxt atp thy css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r e5420161d11d -r 325c8fd0d762 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,21 +26,21 @@ val max_facts_slack = 2 -val all_names = - filter_out (is_likely_tautology orf is_too_meta) +fun all_names ctxt prover = + filter_out (is_likely_tautology ctxt prover orf is_too_meta) #> map (rpair () o Thm.get_name_hint) #> Symtab.make fun evaluate_mash_suggestions ctxt params thy file_name = let val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = Sledgehammer_Isar.default_params ctxt [] - val prover_name = hd provers + val prover = hd provers val slack_max_facts = max_facts_slack * the max_facts val path = file_name |> Path.explode val lines = path |> File.read_lines val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table - val all_names = all_names (facts |> map snd) + val all_names = all_names ctxt prover (facts |> map snd) val iter_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 val mesh_ok = Unsynchronized.ref 0 @@ -80,16 +80,17 @@ val isar_facts = suggested_facts isar_deps facts val iter_facts = Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params - prover_name slack_max_facts NONE hyp_ts concl_t facts + prover slack_max_facts NONE hyp_ts concl_t facts val mash_facts = suggested_facts suggs facts val mess = [(iter_facts, SOME (length iter_facts)), (mash_facts, NONE)] val mesh_facts = mesh_facts slack_max_facts mess fun prove ok heading facts = let val facts = - facts |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t - |> take (the max_facts) - val res as {outcome, ...} = run_prover ctxt params facts goal + facts + |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t + |> take (the max_facts) + val res as {outcome, ...} = run_prover ctxt params prover facts goal val _ = if is_none outcome then ok := !ok + 1 else () in str_of_res heading facts res end val iter_s = prove iter_ok iterN iter_facts @@ -107,7 +108,7 @@ (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts val options = - [prover_name, string_of_int (the max_facts) ^ " facts", + [prover, string_of_int (the max_facts) ^ " facts", "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, the_default "smart" lam_trans, ATP_Util.string_from_time timeout, "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] diff -r e5420161d11d -r 325c8fd0d762 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -10,11 +10,13 @@ type params = Sledgehammer_Provers.params val generate_accessibility : theory -> bool -> string -> unit - val generate_features : Proof.context -> theory -> bool -> string -> unit - val generate_isa_dependencies : theory -> bool -> string -> unit - val generate_atp_dependencies : + val generate_features : + Proof.context -> string -> theory -> bool -> string -> unit + val generate_isa_dependencies : + Proof.context -> string -> theory -> bool -> string -> unit + val generate_prover_dependencies : Proof.context -> params -> theory -> bool -> string -> unit - val generate_commands : Proof.context -> theory -> string -> unit + val generate_commands : Proof.context -> string -> theory -> string -> unit val generate_iter_suggestions : Proof.context -> params -> theory -> int -> string -> unit end; @@ -47,8 +49,8 @@ val thy_name_of_fact = hd o Long_Name.explode fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact -val all_names = - filter_out (is_likely_tautology orf is_too_meta) +fun all_names ctxt prover = + filter_out (is_likely_tautology ctxt prover orf is_too_meta) #> map (rpair () o Thm.get_name_hint) #> Symtab.make fun generate_accessibility thy include_thy file_name = @@ -71,7 +73,7 @@ in fold do_fact facts parents; () end in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end -fun generate_features ctxt thy include_thy file_name = +fun generate_features ctxt prover thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -82,12 +84,13 @@ fun do_fact ((_, (_, status)), th) = let val name = Thm.get_name_hint th - val feats = features_of (theory_of_thm th) status [prop_of th] + val feats = + features_of ctxt prover (theory_of_thm th) status [prop_of th] val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" in File.append path s end in List.app do_fact facts end -fun generate_isa_dependencies thy include_thy file_name = +fun generate_isa_dependencies ctxt prover thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -95,7 +98,7 @@ all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd - val all_names = all_names ths + val all_names = all_names ctxt prover ths fun do_thm th = let val name = Thm.get_name_hint th @@ -104,16 +107,17 @@ in File.append path s end in List.app do_thm ths end -fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy - include_thy file_name = +fun generate_prover_dependencies ctxt (params as {provers, max_facts, ...}) thy + include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" + val prover = hd provers val facts = all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd - val all_names = all_names ths + val all_names = all_names ctxt prover ths fun is_dep dep (_, th) = Thm.get_name_hint th = dep fun add_isa_dep facts dep accum = if exists (is_dep dep) accum then @@ -137,12 +141,12 @@ val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) val facts = - facts |> iterative_relevant_facts ctxt params (hd provers) + facts |> iterative_relevant_facts ctxt params prover (the max_facts) NONE hyp_ts concl_t |> fold (add_isa_dep facts) isa_deps |> map fix_name in - case run_prover ctxt params facts goal of + case run_prover ctxt params prover facts goal of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> sort string_ord | _ => isa_deps @@ -151,7 +155,7 @@ in File.append path s end in List.app do_thm ths end -fun generate_commands ctxt thy file_name = +fun generate_commands ctxt prover thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -161,11 +165,11 @@ facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) val ths = facts |> map snd - val all_names = all_names ths + val all_names = all_names ctxt prover ths fun do_fact ((_, (_, status)), th) prevs = let val name = Thm.get_name_hint th - val feats = features_of thy status [prop_of th] + val feats = features_of ctxt prover thy status [prop_of th] val deps = isabelle_dependencies_of all_names th val kind = Thm.legacy_get_kind th val core = escape_metas prevs ^ "; " ^ escape_metas feats @@ -184,6 +188,7 @@ let val path = file_name |> Path.explode val _ = File.write path "" + val prover = hd provers val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table val (new_facts, old_facts) = @@ -201,7 +206,7 @@ val suggs = old_facts |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params - (hd provers) max_relevant NONE hyp_ts concl_t + prover max_relevant NONE hyp_ts concl_t |> map (fn ((name, _), _) => name ()) |> sort string_ord val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" diff -r e5420161d11d -r 325c8fd0d762 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200 @@ -85,8 +85,8 @@ val invert_const : string -> string val unproxify_const : string -> string val new_skolem_var_name_from_const : string -> string + val atp_logical_consts : string list val atp_irrelevant_consts : string list - val atp_widely_irrelevant_consts : string list val atp_schematic_consts_of : term -> typ list Symtab.table val is_type_enc_higher_order : type_enc -> bool val is_type_enc_polymorphic : type_enc -> bool @@ -390,6 +390,13 @@ nth ss (length ss - 2) end +(* These are ignored anyway by the relevance filter (unless they appear in + higher-order places) but not by the monomorphizer. *) +val atp_logical_consts = + [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, + @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, + @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] + (* These are either simplified away by "Meson.presimplify" (most of the time) or handled specially via "fFalse", "fTrue", ..., "fequal". *) val atp_irrelevant_consts = @@ -397,13 +404,7 @@ @{const_name conj}, @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] -val atp_widely_irrelevant_consts = - atp_irrelevant_consts @ - (* These are ignored anyway by the relevance filter (unless they appear in - higher-order places) but not by the monomorphizer. *) - [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, - @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, - @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] +val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts fun add_schematic_const (x as (_, T)) = Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x diff -r e5420161d11d -r 325c8fd0d762 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,14 +26,16 @@ val extract_query : string -> string * string list val suggested_facts : string list -> fact list -> fact list val mesh_facts : int -> (fact list * int option) list -> fact list - val is_likely_tautology : thm -> bool + val is_likely_tautology : Proof.context -> string -> thm -> bool val is_too_meta : thm -> bool val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order - val features_of : theory -> status -> term list -> string list + val features_of : + Proof.context -> string -> theory -> status -> term list -> string list val isabelle_dependencies_of : unit Symtab.table -> thm -> string list val goal_of_thm : theory -> thm -> thm - val run_prover : Proof.context -> params -> fact list -> thm -> prover_result + val run_prover : + Proof.context -> params -> string -> fact list -> thm -> prover_result val mash_RESET : Proof.context -> unit val mash_INIT : Proof.context -> bool @@ -42,13 +44,14 @@ Proof.context -> bool -> (string * string list * string list * string list) list -> unit val mash_QUERY : - Proof.context -> bool -> string list * string list -> string list + Proof.context -> bool -> int -> string list * string list -> string list val mash_reset : Proof.context -> unit - val mash_can_suggest_facts : Proof.context -> bool + val mash_could_suggest_facts : unit -> bool + val mash_can_suggest_facts : unit -> bool val mash_suggest_facts : - Proof.context -> params -> string -> term list -> term -> fact list + Proof.context -> params -> string -> int -> term list -> term -> fact list -> fact list - val mash_learn_thy : Proof.context -> params -> theory -> real -> unit + val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> unit val mash_learn_proof : Proof.context -> params -> term -> thm list -> fact list -> unit val relevant_facts : @@ -65,6 +68,7 @@ open Sledgehammer_Fact open Sledgehammer_Filter_Iter open Sledgehammer_Provers +open Sledgehammer_Minimize val trace = Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false) @@ -186,10 +190,13 @@ end -fun interesting_terms_types_and_classes term_max_depth type_max_depth ts = +fun interesting_terms_types_and_classes ctxt prover term_max_depth + type_max_depth ts = let val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] - val bad_consts = atp_widely_irrelevant_consts + fun is_bad_const (x as (s, _)) args = + member (op =) atp_logical_consts s orelse + fst (is_built_in_const_for_prover ctxt prover x args) fun add_classes @{sort type} = I | add_classes S = union (op =) (map class_name_of S) fun do_add_type (Type (s, Ts)) = @@ -215,8 +222,8 @@ fun add_patterns t = let val (head, args) = strip_comb t in (case head of - Const (s, T) => - not (member (op =) bad_consts s) ? (add_term t #> add_type T) + Const (x as (_, T)) => + not (is_bad_const x args) ? (add_term t #> add_type T) | Free (_, T) => add_type T | Var (_, T) => add_type T | Abs (_, T, body) => add_type T #> add_patterns body @@ -225,9 +232,9 @@ end in [] |> fold add_patterns ts |> sort string_ord end -fun is_likely_tautology th = - null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso - not (Thm.eq_thm_prop (@{thm ext}, th)) +fun is_likely_tautology ctxt prover th = + null (interesting_terms_types_and_classes ctxt prover 0 ~1 [prop_of th]) + andalso not (Thm.eq_thm_prop (@{thm ext}, th)) (* ### FIXME: optimize *) fun is_too_meta th = @@ -253,9 +260,10 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of thy status ts = +fun features_of ctxt prover thy status ts = thy_feature_name_of (Context.theory_name thy) :: - interesting_terms_types_and_classes term_max_depth type_max_depth ts + interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth + ts |> exists (not o is_lambda_free) ts ? cons "lambdas" |> exists (exists_Const is_exists) ts ? cons "skolems" |> exists (not o is_fo_term thy) ts ? cons "ho" @@ -282,21 +290,22 @@ fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init -fun run_prover ctxt (params as {provers, ...}) facts goal = +fun run_prover ctxt params prover facts goal = let val problem = {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, facts = facts |> map (apfst (apfst (fn name => name ()))) - |> map Sledgehammer_Provers.Untranslated_Fact} - val prover = - Sledgehammer_Minimize.get_minimizing_prover ctxt - Sledgehammer_Provers.Normal (hd provers) + |> map Untranslated_Fact} + val prover = get_minimizing_prover ctxt Normal prover in prover params (K (K (K ""))) problem end (*** Low-level communication with MaSh ***) -val max_preds = 500 +fun write_file write file = + let val path = Path.explode file in + File.write path ""; write (File.append path) + end fun mash_info overlord = if overlord then (getenv "ISABELLE_HOME_USER", "") @@ -311,14 +320,11 @@ " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file in trace_msg ctxt (fn () => "Running " ^ command); + write_file (K ()) log_file; + write_file (K ()) err_file; Isabelle_System.bash command; () end -fun write_file write file = - let val path = Path.explode file in - File.write path ""; write (File.append path) - end - fun run_mash_init ctxt overlord write_access write_feats write_deps = let val info as (temp_dir, serial) = mash_info overlord @@ -331,18 +337,19 @@ run_mash ctxt info ("--init --inputDir " ^ in_dir) end -fun run_mash_commands ctxt overlord save write_cmds read_preds = +fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = let val info as (temp_dir, serial) = mash_info overlord + val sugg_file = temp_dir ^ "/mash_suggs" ^ serial val cmd_file = temp_dir ^ "/mash_commands" ^ serial - val pred_file = temp_dir ^ "/mash_preds" ^ serial in + write_file (K ()) sugg_file; write_file write_cmds cmd_file; run_mash ctxt info - ("--inputFile " ^ cmd_file ^ " --predictions " ^ pred_file ^ - " --numberOfPredictions " ^ string_of_int max_preds ^ + ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ + " --numberOfPredictions " ^ string_of_int max_suggs ^ (if save then " --saveModel" else "")); - read_preds (fn () => File.read_lines (Path.explode pred_file)) + read_suggs (fn () => File.read_lines (Path.explode sugg_file)) end fun str_of_update (name, parents, feats, deps) = @@ -376,14 +383,14 @@ | mash_ADD ctxt overlord upds = (trace_msg ctxt (fn () => "MaSh ADD " ^ elide_string 1000 (space_implode " " (map #1 upds))); - run_mash_commands ctxt overlord true + run_mash_commands ctxt overlord true 0 (fn append => List.app (append o str_of_update) upds) (K ())) -fun mash_QUERY ctxt overlord (query as (_, feats)) = +fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); - run_mash_commands ctxt overlord false + run_mash_commands ctxt overlord false max_suggs (fn append => append (str_of_query query)) - (fn preds => snd (extract_query (List.last (preds ())))) + (fn suggs => snd (extract_query (List.last (suggs ())))) handle List.Empty => []) @@ -423,8 +430,9 @@ let val path = mash_state_path () val thys = Symtab.dest thys - fun line_for_thys comp = AList.find (op =) thys comp |> escape_metas - fun fact_line_for name parents = name :: parents |> escape_metas + val line_for_thys = escape_metas o AList.find (op =) thys + fun fact_line_for name parents = + escape_meta name ^ ": " ^ escape_metas parents val append_fact = File.append path o suffix "\n" oo fact_line_for in File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n"); @@ -450,24 +458,35 @@ end -fun mash_can_suggest_facts (_ : Proof.context) = - mash_home () <> "" andalso not (Graph.is_empty (#fact_graph (mash_get ()))) +fun mash_could_suggest_facts () = mash_home () <> "" +fun mash_can_suggest_facts () = not (Graph.is_empty (#fact_graph (mash_get ()))) -fun parents_wrt facts fact_graph = +fun parents_wrt_facts facts fact_graph = let + val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph)) val facts = - Symtab.empty - |> fold (fn (_, th) => Symtab.update (Thm.get_name_hint th, ())) facts + [] |> fold (cons o Thm.get_name_hint o snd) facts + |> filter (Symtab.defined graph_facts) + |> Graph.all_preds fact_graph + val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end -fun mash_suggest_facts ctxt ({overlord, ...} : params) prover hyp_ts concl_t - facts = +(* Generate more suggestions than requested, because some might be thrown out + later for various reasons and "meshing" gives better results with some + slack. *) +fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) + +fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts + concl_t facts = let val thy = Proof_Context.theory_of ctxt val fact_graph = #fact_graph (mash_get ()) - val parents = parents_wrt facts fact_graph - val feats = features_of thy General (concl_t :: hyp_ts) - val suggs = mash_QUERY ctxt overlord (parents, feats) +val _ = warning (PolyML.makestring (length (fact_graph |> Graph.keys), length (fact_graph |> Graph.maximals), +length (fact_graph |> Graph.minimals))) (*###*) + val parents = parents_wrt_facts facts fact_graph + val feats = features_of ctxt prover thy General (concl_t :: hyp_ts) + val suggs = + mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) in suggested_facts suggs facts end fun add_thys_for thy = @@ -489,9 +508,18 @@ val (deps, graph) = ([], graph) |> fold maybe_add_from deps in ((name, parents, feats, deps) :: upds, graph) end -fun mash_learn_thy ctxt ({overlord, ...} : params) thy timeout = +val pass1_learn_timeout_factor = 0.5 +val pass2_learn_timeout_factor = 10.0 + +(* The timeout is understood in a very slack fashion. *) +fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy + timeout = let - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val timer = Timer.startRealTimer () + val prover = hd provers + fun timed_out frac = + Time.> (Timer.checkRealTimer timer, time_mult frac timeout) + val css_table = clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table val {fact_graph, ...} = mash_get () fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th) @@ -501,20 +529,31 @@ () else let + val n = length new_facts + val _ = + if verbose then + "MaShing " ^ string_of_int n ^ " fact" ^ plural_s n ^ + " (advisory timeout: " ^ string_from_time timeout ^ ")..." + |> Output.urgent_message + else + () val ths = facts |> map snd val all_names = - ths |> filter_out (is_likely_tautology orf is_too_meta) + ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta) |> map (rpair () o Thm.get_name_hint) |> Symtab.make - fun do_fact ((_, (_, status)), th) (parents, upds) = - let - val name = Thm.get_name_hint th - val feats = features_of thy status [prop_of th] - val deps = isabelle_dependencies_of all_names th - val upd = (name, parents, feats, deps) - in ([name], upd :: upds) end - val parents = parents_wrt facts fact_graph - val (_, upds) = (parents, []) |> fold do_fact new_facts ||> rev + fun do_fact _ (accum as (_, true)) = accum + | do_fact ((_, (_, status)), th) ((parents, upds), false) = + let + val name = Thm.get_name_hint th + val feats = features_of ctxt prover thy status [prop_of th] + val deps = isabelle_dependencies_of all_names th + val upd = (name, parents, feats, deps) + in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end + val parents = parents_wrt_facts facts fact_graph + val ((_, upds), _) = + ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev + val n = length upds fun trans {thys, fact_graph} = let val mash_INIT_or_ADD = @@ -526,19 +565,37 @@ {thys = thys |> add_thys_for thy, fact_graph = fact_graph}) end - in mash_map trans end + in + TimeLimit.timeLimit (time_mult pass2_learn_timeout_factor timeout) + mash_map trans + handle TimeLimit.TimeOut => + (if verbose then + "MaSh timed out trying to learn " ^ string_of_int n ^ + " fact" ^ plural_s n ^ " in " ^ + string_from_time (Timer.checkRealTimer timer) ^ "." + |> Output.urgent_message + else + ()); + (if verbose then + "MaSh learned " ^ string_of_int n ^ " fact" ^ plural_s n ^ " in " ^ + string_from_time (Timer.checkRealTimer timer) ^ "." + |> Output.urgent_message + else + ()) + end end -fun mash_learn_proof ctxt ({overlord, ...} : params) t used_ths facts = +fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t used_ths facts = let val thy = Proof_Context.theory_of ctxt - val name = ATP_Util.timestamp () (* should be fairly fresh *) - val feats = features_of thy General [t] + val prover = hd provers + val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *) + val feats = features_of ctxt prover thy General [t] val deps = used_ths |> map Thm.get_name_hint in mash_map (fn {thys, fact_graph} => let - val parents = parents_wrt facts fact_graph + val parents = parents_wrt_facts facts fact_graph val upds = [(name, parents, feats, deps)] val (upds, fact_graph) = ([], fact_graph) |> fold (update_fact_graph ctxt) upds @@ -548,7 +605,13 @@ end) end -fun relevant_facts ctxt (params as {fact_filter, ...}) prover max_facts +(* The threshold should be large enough so that MaSh doesn't kick in for Auto + Sledgehammer and Try. *) +val min_secs_for_learning = 15 +val short_learn_timeout_factor = 0.2 +val long_learn_timeout_factor = 4.0 + +fun relevant_facts ctxt (params as {fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") @@ -558,10 +621,32 @@ [] else let + val thy = Proof_Context.theory_of ctxt + fun maybe_learn can_suggest = + if Time.toSeconds timeout >= min_secs_for_learning then + if Multithreading.enabled () then + let + val factor = + if can_suggest then short_learn_timeout_factor + else long_learn_timeout_factor + in + Future.fork (fn () => mash_learn_thy ctxt params thy + (time_mult factor timeout)); () + end + else + mash_learn_thy ctxt params thy + (time_mult short_learn_timeout_factor timeout) + else + () val fact_filter = case fact_filter of - SOME ff => ff - | NONE => if mash_can_suggest_facts ctxt then meshN else iterN + SOME ff => + (if ff <> iterN then maybe_learn (mash_can_suggest_facts ()) else (); + ff) + | NONE => + if mash_can_suggest_facts () then (maybe_learn true; meshN) + else if mash_could_suggest_facts () then (maybe_learn false; iterN) + else iterN val add_ths = Attrib.eval_thms ctxt add fun prepend_facts ths accepts = ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ @@ -572,7 +657,8 @@ concl_t facts |> (fn facts => (facts, SOME (length facts))) fun mash () = - (facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t, NONE) + (mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts, + NONE) val mess = [] |> (if fact_filter <> mashN then cons (iter ()) else I) |> (if fact_filter <> iterN then cons (mash ()) else I) diff -r e5420161d11d -r 325c8fd0d762 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200 @@ -9,6 +9,7 @@ val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string + val time_mult : real -> Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val subgoal_count : Proof.state -> int @@ -26,6 +27,9 @@ val serial_commas = Try.serial_commas val simplify_spaces = strip_spaces false (K true) +fun time_mult k t = + Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t))) + fun parse_bool_option option name s = (case s of "smart" => if option then NONE else raise Option