# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID b002cc16aa9989dcaa9ce0ecd6647e20e5713e06 # Parent 7682bc885e8aab076df6edfc2b5cb238479dd80f honor suggested MaSh weights diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:46 2012 +0200 @@ -133,7 +133,7 @@ Sledgehammer_Fact.no_fact_override reserved css_table chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_MePo.iterative_relevant_facts ctxt params + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params default_prover (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t |> map ((fn name => name ()) o fst o fst) diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200 @@ -115,7 +115,7 @@ fun all_non_tautological_facts_of thy css_table = Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table - |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd) + |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd) fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200 @@ -78,26 +78,28 @@ val isar_deps = isar_dependencies_of all_names th |> these val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) val mepo_facts = - Sledgehammer_MePo.iterative_relevant_facts ctxt params prover + Sledgehammer_MePo.mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts concl_t facts - val mash_facts = facts |> suggested_facts suggs + |> Sledgehammer_MePo.weight_mepo_facts + val mash_facts = suggested_facts suggs facts val mess = [(mepo_facts, []), (mash_facts, [])] val mesh_facts = mesh_facts slack_max_facts mess - val isar_facts = suggested_facts isar_deps facts - fun prove ok heading facts = + val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts + fun prove ok heading get facts = let val facts = - facts - |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t - |> take (the max_facts) + facts |> map get + |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts + concl_t + |> take (the max_facts) val res as {outcome, ...} = run_prover_for_mash ctxt params prover facts goal val _ = if is_none outcome then ok := !ok + 1 else () in str_of_res heading facts res end - val mepo_s = prove mepo_ok MePoN mepo_facts - val mash_s = prove mash_ok MaShN mash_facts - val mesh_s = prove mesh_ok MeshN mesh_facts - val isar_s = prove isar_ok IsarN isar_facts + val mepo_s = prove mepo_ok MePoN fst mepo_facts + val mash_s = prove mash_ok MaShN fst mash_facts + val mesh_s = prove mesh_ok MeshN I mesh_facts + val isar_s = prove isar_ok IsarN fst isar_facts in ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, isar_s] diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200 @@ -179,7 +179,7 @@ let val suggs = old_facts - |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover max_relevant NONE hyp_ts concl_t |> map (fn ((name, _), _) => name ()) val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200 @@ -23,6 +23,7 @@ val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list + val is_likely_tautology_or_too_meta : thm -> bool val backquote_thm : thm -> string val clasimpset_rule_table_of : Proof.context -> status Termtab.table val maybe_instantiate_inducts : @@ -210,6 +211,24 @@ is_that_fact thm end +fun is_likely_tautology_or_too_meta th = + let + val is_boring_const = member (op =) atp_widely_irrelevant_consts + fun is_boring_bool t = + not (exists_Const (not o is_boring_const o fst) t) orelse + exists_type (exists_subtype (curry (op =) @{typ prop})) t + fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t + | is_boring_prop (@{const "==>"} $ t $ u) = + is_boring_prop t andalso is_boring_prop u + | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = + is_boring_prop t andalso is_boring_prop u + | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = + is_boring_bool t andalso is_boring_bool u + | is_boring_prop _ = true + in + is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) + end + fun hackish_string_for_term thy t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) (Syntax.string_of_term_global thy) t @@ -439,6 +458,7 @@ else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in all_facts ctxt ho_atp reserved add chained css + |> filter_out (is_likely_tautology_or_too_meta o snd) |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt |> uniquify diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 @@ -218,7 +218,7 @@ val max_local_and_remote = max_local_and_remote |> (if String.isPrefix remote_prefix prover then apsnd else apfst) - (Integer.add ~1) + (Integer.add ~1) in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end val max_default_remote_threads = 4 diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 @@ -28,12 +28,12 @@ val escape_metas : string list -> string val unescape_meta : string -> string val unescape_metas : string -> string list - val extract_query : string -> string * string list + val extract_query : string -> string * (string * real) list val nickname_of : thm -> string - val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list + val suggested_facts : + (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list val mesh_facts : - int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list - val is_likely_tautology_or_too_meta : thm -> bool + int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order val goal_of_thm : theory -> thm -> thm @@ -52,13 +52,14 @@ val mash_REPROVE : Proof.context -> bool -> (string * string list) list -> unit val mash_QUERY : - Proof.context -> bool -> int -> string list * string list -> string list + Proof.context -> bool -> int -> string list * string list + -> (string * real) list val mash_unlearn : Proof.context -> unit val mash_could_suggest_facts : unit -> bool val mash_can_suggest_facts : Proof.context -> bool - val mash_suggest_facts : + val mash_suggested_facts : Proof.context -> params -> string -> int -> term list -> term - -> ('a * thm) list -> ('a * thm) list * ('a * thm) list + -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list val mash_learn_proof : Proof.context -> params -> string -> term -> ('a * thm) list -> thm list -> unit @@ -132,9 +133,22 @@ val unescape_metas = space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta +fun extract_node line = + case space_explode ":" line of + [name, parents] => (unescape_meta name, unescape_metas parents) + | _ => ("", []) + +fun extract_suggestion sugg = + case space_explode "=" sugg of + [name, weight] => + SOME (unescape_meta name, Real.fromString weight |> the_default 0.0) + | _ => NONE + fun extract_query line = case space_explode ":" line of - [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) + [goal, suggs] => + (unescape_meta goal, + map_filter extract_suggestion (space_explode " " suggs)) | _ => ("", []) fun parent_of_local_thm th = @@ -165,31 +179,35 @@ let fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) val tab = Symtab.empty |> fold add_fact facts - in map_filter (Symtab.lookup tab) suggs end + fun find_sugg (name, weight) = + Symtab.lookup tab name |> Option.map (rpair weight) + in map_filter find_sugg suggs end -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) -fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0 +fun sum_avg [] = 0 + | sum_avg xs = Real.ceil (100000.0 * fold (curry (op +)) xs 0.0) div length xs -fun sum_sq_avg [] = 0 - | sum_sq_avg xs = - Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs +fun normalize_scores [] = [] + | normalize_scores ((fact, score) :: tail) = + (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail -fun mesh_facts max_facts [(selected, unknown)] = - take max_facts selected @ take (max_facts - length selected) unknown +fun mesh_facts max_facts [(sels, unks)] = + map fst (take max_facts sels) @ take (max_facts - length sels) unks | mesh_facts max_facts mess = let - val mess = mess |> map (apfst (`length)) + val mess = mess |> map (apfst (normalize_scores #> `length)) val fact_eq = Thm.eq_thm o pairself snd + fun score_at sels = try (nth sels) #> Option.map snd fun score_in fact ((sel_len, sels), unks) = - case find_index (curry fact_eq fact) sels of + case find_index (curry fact_eq fact o fst) sels of ~1 => (case find_index (curry fact_eq fact) unks of - ~1 => SOME sel_len + ~1 => score_at sels sel_len | _ => NONE) - | j => SOME j - fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg - val facts = fold (union fact_eq o take max_facts o snd o fst) mess [] + | rank => score_at sels rank + fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg + val facts = + fold (union fact_eq o map fst o take max_facts o snd o fst) mess [] in - facts |> map (`score_of) |> sort (int_ord o swap o pairself fst) + facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |> map snd |> take max_facts end @@ -198,24 +216,6 @@ val type_name_of = prefix "t" val class_name_of = prefix "s" -fun is_likely_tautology_or_too_meta th = - let - val is_boring_const = member (op =) atp_widely_irrelevant_consts - fun is_boring_bool t = - not (exists_Const (not o is_boring_const o fst) t) orelse - exists_type (exists_subtype (curry (op =) @{typ prop})) t - fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t - | is_boring_prop (@{const "==>"} $ t $ u) = - is_boring_prop t andalso is_boring_prop u - | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = - is_boring_prop t andalso is_boring_prop u - | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = - is_boring_bool t andalso is_boring_bool u - | is_boring_prop _ = true - in - is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) - end - fun theory_ord p = if Theory.eq_thy p then EQUAL @@ -280,10 +280,11 @@ if is_bad_const x args then "" else mk_app (const_name_of s) (map (patternify (depth - 1)) args) | _ => "" + fun add_pattern depth t = + case patternify depth t of "" => I | s => insert (op =) s fun add_term_patterns ~1 _ = I | add_term_patterns depth t = - insert (op =) (patternify depth t) - #> add_term_patterns (depth - 1) t + add_pattern depth t #> add_term_patterns (depth - 1) t val add_term = add_term_patterns term_max_depth fun add_patterns t = let val (head, args) = strip_comb t in @@ -327,8 +328,8 @@ fun trim_dependencies deps = if length deps <= max_dependencies then SOME deps else NONE -fun isar_dependencies_of all_facts = - thms_in_proof (SOME all_facts) #> trim_dependencies +fun isar_dependencies_of all_names = + thms_in_proof (SOME all_names) #> trim_dependencies fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts all_names th = @@ -349,7 +350,7 @@ SOME ((name, status), th) => accum @ [((name, status), th)] | NONE => accum (* shouldn't happen *) val facts = - facts |> iterative_relevant_facts ctxt params prover + facts |> mepo_suggested_facts ctxt params prover (max_facts |> the_default atp_dependency_default_max_fact) NONE hyp_ts concl_t |> fold (add_isar_dep facts) (these isar_deps) @@ -432,7 +433,7 @@ "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" fun str_of_query (parents, feats) = - "? " ^ escape_metas parents ^ "; " ^ escape_metas feats + "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n" fun mash_CLEAR ctxt = let val path = mash_model_dir () |> Path.explode in @@ -487,6 +488,13 @@ "Internal error when " ^ when ^ ":\n" ^ ML_Compiler.exn_message exn); def) +fun graph_info G = + string_of_int (length (Graph.keys G)) ^ " node(s), " ^ + string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ + " edge(s), " ^ + string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ + string_of_int (length (Graph.maximals G)) ^ " maximal" + type mash_state = {fact_G : unit Graph.T} val empty_state = {fact_G = Graph.empty} @@ -500,26 +508,27 @@ let val path = mash_state_path () in (true, case try File.read_lines path of - SOME (version' :: fact_lines) => + SOME (version' :: node_lines) => let fun add_edge_to name parent = - Graph.default_node (parent, ()) - #> Graph.add_edge (parent, name) - fun add_fact_line line = - case extract_query line of + Graph.default_node (parent, ()) #> Graph.add_edge (parent, name) + fun add_node line = + case extract_node line of ("", _) => I (* shouldn't happen *) | (name, parents) => - Graph.default_node (name, ()) - #> fold (add_edge_to name) parents + Graph.default_node (name, ()) #> fold (add_edge_to name) parents val fact_G = try_graph ctxt "loading state" Graph.empty (fn () => - Graph.empty |> version' = version - ? fold add_fact_line fact_lines) - in {fact_G = fact_G} end + Graph.empty |> version' = version ? fold add_node node_lines) + in + trace_msg ctxt (fn () => + "Loaded fact graph (" ^ graph_info fact_G ^ ")"); + {fact_G = fact_G} + end | _ => empty_state) end -fun save {fact_G} = +fun save ctxt {fact_G} = let val path = mash_state_path () fun fact_line_for name parents = @@ -529,7 +538,8 @@ append_fact name (Graph.Keys.dest parents) in File.write path (version ^ "\n"); - Graph.fold append_entry fact_G () + Graph.fold append_entry fact_G (); + trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")") end val global_state = @@ -538,7 +548,7 @@ in fun mash_map ctxt f = - Synchronized.change global_state (load ctxt ##> (f #> tap save)) + Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt))) fun mash_get ctxt = Synchronized.change_result global_state (load ctxt #> `snd) @@ -567,9 +577,11 @@ if Symtab.defined tab name then let val new = (Graph.all_preds fact_G [name], name) - fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x) - val maxs = maxs |> filter (fn max => not_ancestor max new) - val maxs = maxs |> forall (not_ancestor new) maxs ? cons new + fun is_ancestor (_, x) (yp, _) = member (op =) yp x + val maxs = maxs |> filter (fn max => not (is_ancestor max new)) + val maxs = + if exists (is_ancestor new) maxs then maxs + else new :: filter_out (fn max => is_ancestor max new) maxs in find_maxes (name :: seen) maxs names end else find_maxes (name :: seen) maxs @@ -585,8 +597,8 @@ fun is_fact_in_graph fact_G (_, th) = can (Graph.get_node fact_G) (nickname_of th) -fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts - concl_t facts = +fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts + concl_t facts = let val thy = Proof_Context.theory_of ctxt val fact_G = #fact_G (mash_get ctxt) @@ -756,13 +768,13 @@ n else let - fun score_of (_, th) = + fun priority_of (_, th) = random_range 0 (1000 * max_dependencies) - 500 * (th |> isar_dependencies_of all_names |> Option.map length |> the_default max_dependencies) val old_facts = - old_facts |> map (`score_of) + old_facts |> map (`priority_of) |> sort (int_ord o pairself fst) |> map snd val (reps, (n, _, _)) = @@ -850,13 +862,14 @@ ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ (accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |> take max_facts - fun iter () = - iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts - concl_t facts + fun mepo () = + facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts + concl_t + |> weight_mepo_facts fun mash () = - mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts + mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts val mess = - [] |> (if fact_filter <> mashN then cons (iter (), []) else I) + [] |> (if fact_filter <> mashN then cons (mepo (), []) else I) |> (if fact_filter <> mepoN then cons (mash ()) else I) in mesh_facts max_facts mess diff -r 7682bc885e8a -r b002cc16aa99 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:46 2012 +0200 @@ -18,9 +18,10 @@ val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list - val iterative_relevant_facts : + val mepo_suggested_facts : Proof.context -> params -> string -> int -> relevance_fudge option -> term list -> term -> fact list -> fact list + val weight_mepo_facts : fact list -> (fact * real) list end; structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = @@ -508,7 +509,7 @@ "Total relevant: " ^ string_of_int (length accepts))) end -fun iterative_relevant_facts ctxt +fun mepo_suggested_facts ctxt ({fact_thresholds = (thres0, thres1), ...} : params) prover max_facts fudge hyp_ts concl_t facts = let @@ -534,4 +535,11 @@ (concl_t |> theory_constify fudge (Context.theory_name thy))) end +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) +fun weight_of_fact rank = + Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0 + +fun weight_mepo_facts facts = + facts ~~ map weight_of_fact (0 upto length facts - 1) + end;