# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID 47fe0ca12fc2c2a6ea0991bb62edf249f7748a4e # Parent b002cc16aa9989dcaa9ce0ecd6647e20e5713e06 faster maximal node computation diff -r b002cc16aa99 -r 47fe0ca12fc2 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 @@ -184,7 +184,8 @@ in map_filter find_sugg suggs end fun sum_avg [] = 0 - | sum_avg xs = Real.ceil (100000.0 * fold (curry (op +)) xs 0.0) div length xs + | sum_avg xs = + Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs fun normalize_scores [] = [] | normalize_scores ((fact, score) :: tail) = @@ -562,32 +563,37 @@ fun mash_could_suggest_facts () = mash_home () <> "" fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) -fun queue_of xs = Queue.empty |> fold Queue.enqueue xs +fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 -fun max_facts_in_graph fact_G facts = +fun maximal_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 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 => map snd maxs - | SOME (name, names) => - if Symtab.defined tab name then - let - val new = (Graph.all_preds fact_G [name], name) - 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 - (Graph.Keys.fold (enqueue_new seen) - (Graph.imm_preds fact_G name) names) - in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end + val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts + fun insert_new seen name = + not (Symtab.defined seen name) ? insert (op =) name + fun find_maxes _ (maxs, []) = map snd maxs + | find_maxes seen (maxs, new :: news) = + find_maxes + (seen |> num_keys (Graph.imm_succs fact_G new) > 1 + ? Symtab.default (new, ())) + (if Symtab.defined tab new then + let + val newp = Graph.all_preds fact_G [new] + fun is_ancestor x yp = member (op =) yp x + val maxs = + maxs |> filter (fn (_, max) => not (is_ancestor max newp)) + in + if exists (is_ancestor new o fst) maxs then + (maxs, news) + else + ((newp, new) + :: filter_out (fn (_, max) => is_ancestor max newp) maxs, + news) + end + else + (maxs, Graph.Keys.fold (insert_new seen) + (Graph.imm_preds fact_G new) news)) + in find_maxes Symtab.empty ([], 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 @@ -602,7 +608,7 @@ let val thy = Proof_Context.theory_of ctxt val fact_G = #fact_G (mash_get ctxt) - val parents = max_facts_in_graph fact_G facts + val parents = maximal_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_G then [] @@ -618,7 +624,7 @@ (from :: parents, Graph.add_edge_acyclic (from, name) graph)) val graph = graph |> Graph.default_node (name, ()) val (parents, graph) = ([], graph) |> fold maybe_add_from parents - val (deps, graph) = ([], graph) |> fold maybe_add_from deps + val (deps, _) = ([], graph) |> fold maybe_add_from deps in ((name, parents, feats, deps) :: adds, graph) end val learn_timeout_slack = 2.0 @@ -647,7 +653,7 @@ val feats = features_of ctxt prover thy (Local, General) [t] val deps = used_ths |> map nickname_of val {fact_G} = mash_get ctxt - val parents = max_facts_in_graph fact_G facts + val parents = timeit (fn () => maximal_in_graph fact_G facts) in mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "") end) @@ -743,7 +749,7 @@ val ancestors = old_facts |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) - val parents = max_facts_in_graph fact_G ancestors + val parents = maximal_in_graph fact_G ancestors val (adds, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) |> fold learn_new_fact new_facts @@ -853,10 +859,13 @@ case fact_filter of SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) | NONE => - if is_smt_prover ctxt prover then mepoN - else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) - else if mash_could_suggest_facts () then (maybe_learn (); mepoN) - else mepoN + if is_smt_prover ctxt prover then + mepoN + else if mash_could_suggest_facts () then + (maybe_learn (); + if mash_can_suggest_facts ctxt then meshN else mepoN) + else + mepoN val add_ths = Attrib.eval_thms ctxt add fun prepend_facts ths accepts = ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ diff -r b002cc16aa99 -r 47fe0ca12fc2 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 @@ -64,8 +64,8 @@ fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, timeout, expect, ...}) - mode minimize_command only {state, goal, subgoal, subgoal_count, facts} - name = + mode minimize_command only learn + {state, goal, subgoal, subgoal_count, facts} name = let val ctxt = Proof.context_of state val hard_timeout = Time.+ (timeout, timeout) @@ -93,9 +93,6 @@ |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ " proof (of " ^ string_of_int (length facts) ^ "): ") "." |> Output.urgent_message - fun learn prover = - mash_learn_proof ctxt params prover (prop_of goal) - (map untranslated_fact facts) fun really_go () = problem |> get_minimizing_prover ctxt mode learn name params minimize_command @@ -188,7 +185,7 @@ val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers val reserved = reserved_isar_keyword_table () val css = clasimpset_rule_table_of ctxt - val facts = + val all_facts = nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t val _ = () |> not blocking ? kill_provers @@ -208,7 +205,9 @@ val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts} - val launch = launch_prover params mode minimize_command only + fun learn prover = + mash_learn_proof ctxt params prover (prop_of goal) all_facts + val launch = launch_prover params mode minimize_command only learn in if mode = Auto_Try orelse mode = Try then (unknownN, state) @@ -232,7 +231,7 @@ provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) in - facts + all_facts |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I)