# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID f08425165cca31a5782c19f912729eca56cfa57c # Parent 4bacc8983b3d50636c5eea85010ba070390e59cf minimal maxes + tuning diff -r 4bacc8983b3d -r f08425165cca 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 @@ -238,10 +238,12 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst -fun backquote_thm th = - th |> prop_of |> close_form - |> hackish_string_for_term (theory_of_thm th) - |> backquote +fun backquote_term thy t = + t |> close_form + |> hackish_string_for_term thy + |> backquote + +fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th) fun clasimpset_rule_table_of ctxt = let diff -r 4bacc8983b3d -r f08425165cca 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 @@ -167,9 +167,10 @@ ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) - else case Int.fromString name of - SOME n => ("max_facts", [name]) - | NONE => error ("Unknown parameter: " ^ quote name ^ ".")) + else if can Int.fromString name then + ("max_facts", [name]) + else + error ("Unknown parameter: " ^ quote name ^ ".")) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are @@ -375,7 +376,7 @@ let val ctxt = ctxt |> Config.put instantiate_inducts false val i = the_default 1 opt_i - val params as {provers, ...} = + val params = get_params Minimize ctxt (("provers", [default_minimize_prover]) :: override_params) val goal = prop_of (#goal (Proof.goal state)) diff -r 4bacc8983b3d -r f08425165cca 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 @@ -472,9 +472,9 @@ "Internal error when " ^ when ^ ":\n" ^ ML_Compiler.exn_message exn); def) -type mash_state = {fact_graph : unit Graph.T} +type mash_state = {fact_G : unit Graph.T} -val empty_state = {fact_graph = Graph.empty} +val empty_state = {fact_G = Graph.empty} local @@ -496,25 +496,25 @@ | (name, parents) => Graph.default_node (name, ()) #> fold (add_edge_to name) parents - val fact_graph = + val fact_G = try_graph ctxt "loading state" Graph.empty (fn () => Graph.empty |> version' = version ? fold add_fact_line fact_lines) - in {fact_graph = fact_graph} end + in {fact_G = fact_G} end | _ => empty_state) end -fun save {fact_graph} = +fun save {fact_G} = let val path = mash_state_path () 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 + fun append_entry (name, ((), (parents, _))) () = + append_fact name (Graph.Keys.dest parents) in File.write path (version ^ "\n"); - Graph.fold (fn (name, ((), (parents, _))) => fn () => - append_fact name (Graph.Keys.dest parents)) - fact_graph () + Graph.fold append_entry fact_G () end val global_state = @@ -535,45 +535,52 @@ end fun mash_could_suggest_facts () = mash_home () <> "" -fun mash_can_suggest_facts ctxt = - not (Graph.is_empty (#fact_graph (mash_get ctxt))) +fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) -fun parents_wrt_facts facts fact_graph = +fun queue_of xs = Queue.empty |> fold Queue.enqueue xs + +fun max_facts_in_graph fact_G facts = let val facts = [] |> fold (cons o nickname_of o snd) facts val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts - fun insert_not_seen seen name = - not (member (op =) seen name) ? insert (op =) name - fun parents_of _ parents [] = parents - | parents_of seen parents (name :: names) = - if Symtab.defined tab name then - parents_of (name :: seen) (name :: parents) names - else - parents_of (name :: seen) parents - (Graph.Keys.fold (insert_not_seen seen) - (Graph.imm_preds fact_graph name) names) - in parents_of [] [] (Graph.maximals fact_graph) end + fun enqueue_new seen name = + not (member (op =) seen name) ? Queue.enqueue name + fun find_maxes seen maxs names = + case try Queue.dequeue names of + NONE => maxs + | SOME (name, names) => + if Symtab.defined tab name then + let + fun no_path x y = not (member (op =) (Graph.all_preds fact_G [y]) x) + val maxs = maxs |> filter (fn max => no_path max name) + val maxs = maxs |> forall (no_path name) maxs ? cons name + in find_maxes (name :: seen) maxs names end + else + find_maxes (name :: seen) maxs + (Graph.Keys.fold (enqueue_new seen) + (Graph.imm_preds fact_G name) names) + in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end (* 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 is_fact_in_graph fact_graph (_, th) = - can (Graph.get_node fact_graph) (nickname_of th) +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 = let val thy = Proof_Context.theory_of ctxt - val fact_graph = #fact_graph (mash_get ctxt) - val parents = parents_wrt_facts facts fact_graph + val fact_G = #fact_G (mash_get ctxt) + val parents = max_facts_in_graph fact_G facts val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) val suggs = - if Graph.is_empty fact_graph then [] + if Graph.is_empty fact_G then [] else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) val selected = facts |> suggested_facts suggs - val unknown = facts |> filter_out (is_fact_in_graph fact_graph) + val unknown = facts |> filter_out (is_fact_in_graph fact_G) in (selected, unknown) end fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) = @@ -596,6 +603,10 @@ val desc = ("machine learner for Sledgehammer", "") in Async_Manager.launch MaShN birth_time death_time desc task end +fun freshish_name () = + Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^ + serial_string () + fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts used_ths = if is_smt_prover ctxt prover then @@ -605,18 +616,17 @@ (fn () => let val thy = Proof_Context.theory_of ctxt - val name = timestamp () ^ " " ^ serial_string () (* freshish *) + val name = freshish_name () val feats = features_of ctxt prover thy (Local, General) [t] val deps = used_ths |> map nickname_of in - mash_map ctxt (fn {fact_graph} => + mash_map ctxt (fn {fact_G} => let - val parents = parents_wrt_facts facts fact_graph + val parents = max_facts_in_graph fact_G facts val upds = [(name, parents, feats, deps)] - val (upds, fact_graph) = - ([], fact_graph) |> fold (update_fact_graph ctxt) upds - in - mash_ADD ctxt overlord upds; {fact_graph = fact_graph} + val (upds, fact_G) = + ([], fact_G) |> fold (update_fact_graph ctxt) upds + in mash_ADD ctxt overlord upds; {fact_G = fact_G} end); (true, "") end) @@ -636,10 +646,10 @@ val timer = Timer.startRealTimer () fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout) - val {fact_graph} = mash_get ctxt - val new_facts = - facts |> filter_out (is_fact_in_graph fact_graph) - |> sort (thm_ord o pairself snd) + val {fact_G} = mash_get ctxt + val (old_facts, new_facts) = + facts |> List.partition (is_fact_in_graph fact_G) + ||> sort (thm_ord o pairself snd) val num_new_facts = length new_facts in (if not auto then @@ -654,7 +664,7 @@ else "") |> Output.urgent_message; - if null new_facts then + if num_new_facts = 0 then if not auto then "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^ sendback relearn_atpN ^ " to learn from scratch." @@ -662,17 +672,21 @@ "" else let - val ths = facts |> map snd + val last_th = new_facts |> List.last |> snd + (* crude approximation *) + val ancestors = + old_facts |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) val all_names = - ths |> filter_out is_likely_tautology_or_too_meta - |> map (rpair () o nickname_of) - |> Symtab.make + facts |> map snd + |> filter_out is_likely_tautology_or_too_meta + |> map (rpair () o nickname_of) + |> Symtab.make fun do_commit [] state = state - | do_commit upds {fact_graph} = + | do_commit upds {fact_G} = let - val (upds, fact_graph) = - ([], fact_graph) |> fold (update_fact_graph ctxt) upds - in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end + val (upds, fact_G) = + ([], fact_G) |> fold (update_fact_graph ctxt) upds + in mash_ADD ctxt overlord (rev upds); {fact_G = fact_G} end fun trim_deps deps = if length deps > max_dependencies then [] else deps fun commit last upds = (if debug andalso not auto then Output.urgent_message "Committing..." @@ -708,7 +722,7 @@ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) in (upds, ([name], n, next_commit, timed_out)) end - val parents = parents_wrt_facts facts fact_graph + val parents = max_facts_in_graph fact_G ancestors val (upds, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) |> fold do_fact new_facts