# HG changeset patch # User blanchet # Date 1404059307 -7200 # Node ID 78d7fbe9b20342c9415476467436c415495c1444 # Parent 02c408aed5eecff8c8ec28263c62b23da415f8f2 tuning diff -r 02c408aed5ee -r 78d7fbe9b203 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200 @@ -47,7 +47,9 @@ val zeros = [0, 0, 0, 0, 0, 0] val report_path = report_file_name |> Path.explode val _ = File.write report_path "" + fun print s = File.append report_path (s ^ "\n") + val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy [] val prover = hd provers val max_suggs = generous_max_suggestions (the max_facts) @@ -59,18 +61,21 @@ mesh_isar_lines, mesh_prover_lines] = map lines_of file_names val num_lines = fold (Integer.max o length) lines 0 + fun pad lines = lines @ replicate (num_lines - length lines) "" + val lines = pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~ pad mesh_isar_lines ~~ pad mesh_prover_lines val css = clasimpset_rule_table_of ctxt val facts = all_facts ctxt true false Symtab.empty [] [] css val name_tabs = build_name_tables nickname_of_thm facts + fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_str (j, s) = s ^ "@" ^ string_of_int j val str_of_method = enclose " " ": " - fun str_of_result method facts ({outcome, run_time, used_facts, ...} - : prover_result) = + + fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) = let val facts = facts |> map (fst o fst) in str_of_method method ^ (if is_none outcome then @@ -89,8 +94,9 @@ |> map index_str |> space_implode " ")) end - fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), - mesh_isar_line), mesh_prover_line)) = + + fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), mesh_isar_line), + mesh_prover_line)) = if in_range range j then let val get_suggs = extract_suggestions ##> (take max_suggs #> map fst) @@ -111,18 +117,18 @@ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = these (isar_dependencies_of name_tabs th) val facts = facts |> filter (fn (_, th') => thm_less (th', th)) + (* adapted from "mirabelle_sledgehammer.ML" *) fun set_file_name method (SOME dir) = let - val prob_prefix = - "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ - method + val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method in Config.put atp_dest_dir dir #> Config.put atp_problem_prefix (prob_prefix ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) end | set_file_name _ NONE = I + fun prove method suggs = if not (member (op =) methods method) orelse (null facts andalso method <> IsarN) then @@ -131,6 +137,7 @@ let fun nickify ((_, stature), th) = ((K (encode_str (nickname_of_thm th)), stature), th) + val facts = suggs |> find_suggested_facts ctxt facts @@ -142,7 +149,10 @@ val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal val ok = if is_none outcome then 1 else 0 - in (str_of_result method facts res, ok) end + in + (str_of_result method facts res, ok) + end + val ress = [fn () => prove MePoN mepo_suggs, fn () => prove MaSh_IsarN mash_isar_suggs, @@ -158,10 +168,12 @@ end else zeros + fun total_of method ok n = str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)" + val inst_inducts = Config.get ctxt instantiate_inducts val options = ["prover = " ^ prover, @@ -175,8 +187,7 @@ val _ = print ("Options: " ^ commas options); val oks = Par_List.map solve_goal (tag_list 1 lines) val n = length oks - val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, - isar_ok] = + val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, isar_ok] = if n = 0 then zeros else map Integer.sum (map_transpose I oks) in ["Successes (of " ^ string_of_int n ^ " goals)", diff -r 02c408aed5ee -r 78d7fbe9b203 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sun Jun 29 18:28:27 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Sun Jun 29 18:28:27 2014 +0200 @@ -40,6 +40,11 @@ fun in_range (from, to) j = j >= from andalso (to = NONE orelse j <= the to) +fun encode_feature (names, weight) = + encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight) + +val encode_features = map encode_feature #> space_implode " " + (* The suggested weights do not make much sense. *) fun extract_suggestion sugg = (case space_explode "=" sugg of diff -r 02c408aed5ee -r 78d7fbe9b203 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 29 18:28:27 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 29 18:28:27 2014 +0200 @@ -32,7 +32,6 @@ val encode_strs : string list -> string val decode_str : string -> string val decode_strs : string -> string list - val encode_features : (string * real) list -> string datatype mash_engine = MaSh_kNN @@ -62,8 +61,8 @@ val extra_feature_factor : real val weight_facts_smoothly : 'a list -> ('a * real) list val weight_facts_steeply : 'a list -> ('a * real) list - val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list -> - ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list + val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> + ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list @@ -72,8 +71,8 @@ val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> raw_fact list -> string val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit + val mash_can_suggest_facts : Proof.context -> bool - val mash_can_suggest_facts : Proof.context -> bool val generous_max_suggestions : int -> int val mepo_weight : real val mash_weight : real @@ -160,36 +159,6 @@ val the_mash_engine = the_default MaSh_NB o mash_engine -(*** Maintenance of the persistent, string-based state ***) - -fun meta_char c = - if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse - c = #"," then - String.str c - else - (* fixed width, in case more digits follow *) - "%" ^ stringN_of_int 3 (Char.ord c) - -fun unmeta_chars accum [] = String.implode (rev accum) - | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = - (case Int.fromString (String.implode [d1, d2, d3]) of - SOME n => unmeta_chars (Char.chr n :: accum) cs - | NONE => "" (* error *)) - | unmeta_chars _ (#"%" :: _) = "" (* error *) - | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs - -val encode_str = String.translate meta_char -val decode_str = String.explode #> unmeta_chars [] - -val encode_strs = map encode_str #> space_implode " " -val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str - -fun encode_feature (names, weight) = - encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight) - -val encode_features = map encode_feature #> space_implode " " - - (*** Isabelle-agnostic machine learning ***) structure MaSh = @@ -464,14 +433,14 @@ val naive_bayes_ext = external_tool "predict/nbayes" fun query_external ctxt engine max_suggs learns goal_feats = - (trace_msg ctxt (fn () => "MaSh query external " ^ encode_features goal_feats); + (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats)); (case engine of MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats | MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats)) fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss) (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats = - (trace_msg ctxt (fn () => "MaSh query internal " ^ encode_features goal_feats ^ " from {" ^ + (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^ elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}"); (case engine of MaSh_kNN => @@ -490,7 +459,29 @@ end; -(*** Middle-level communication with MaSh ***) +(*** Persistent, stringly-typed state ***) + +fun meta_char c = + if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse + c = #"," then + String.str c + else + (* fixed width, in case more digits follow *) + "%" ^ stringN_of_int 3 (Char.ord c) + +fun unmeta_chars accum [] = String.implode (rev accum) + | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = + (case Int.fromString (String.implode [d1, d2, d3]) of + SOME n => unmeta_chars (Char.chr n :: accum) cs + | NONE => "" (* error *)) + | unmeta_chars _ (#"%" :: _) = "" (* error *) + | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs + +val encode_str = String.translate meta_char +val decode_str = String.explode #> unmeta_chars [] + +val encode_strs = map encode_str #> space_implode " " +val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop