1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -184,7 +184,8 @@
1.4 in map_filter find_sugg suggs end
1.5
1.6 fun sum_avg [] = 0
1.7 - | sum_avg xs = Real.ceil (100000.0 * fold (curry (op +)) xs 0.0) div length xs
1.8 + | sum_avg xs =
1.9 + Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
1.10
1.11 fun normalize_scores [] = []
1.12 | normalize_scores ((fact, score) :: tail) =
1.13 @@ -562,32 +563,37 @@
1.14 fun mash_could_suggest_facts () = mash_home () <> ""
1.15 fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
1.16
1.17 -fun queue_of xs = Queue.empty |> fold Queue.enqueue xs
1.18 +fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
1.19
1.20 -fun max_facts_in_graph fact_G facts =
1.21 +fun maximal_in_graph fact_G facts =
1.22 let
1.23 val facts = [] |> fold (cons o nickname_of o snd) facts
1.24 - val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
1.25 - fun enqueue_new seen name =
1.26 - not (member (op =) seen name) ? Queue.enqueue name
1.27 - fun find_maxes seen maxs names =
1.28 - case try Queue.dequeue names of
1.29 - NONE => map snd maxs
1.30 - | SOME (name, names) =>
1.31 - if Symtab.defined tab name then
1.32 - let
1.33 - val new = (Graph.all_preds fact_G [name], name)
1.34 - fun is_ancestor (_, x) (yp, _) = member (op =) yp x
1.35 - val maxs = maxs |> filter (fn max => not (is_ancestor max new))
1.36 - val maxs =
1.37 - if exists (is_ancestor new) maxs then maxs
1.38 - else new :: filter_out (fn max => is_ancestor max new) maxs
1.39 - in find_maxes (name :: seen) maxs names end
1.40 - else
1.41 - find_maxes (name :: seen) maxs
1.42 - (Graph.Keys.fold (enqueue_new seen)
1.43 - (Graph.imm_preds fact_G name) names)
1.44 - in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end
1.45 + val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
1.46 + fun insert_new seen name =
1.47 + not (Symtab.defined seen name) ? insert (op =) name
1.48 + fun find_maxes _ (maxs, []) = map snd maxs
1.49 + | find_maxes seen (maxs, new :: news) =
1.50 + find_maxes
1.51 + (seen |> num_keys (Graph.imm_succs fact_G new) > 1
1.52 + ? Symtab.default (new, ()))
1.53 + (if Symtab.defined tab new then
1.54 + let
1.55 + val newp = Graph.all_preds fact_G [new]
1.56 + fun is_ancestor x yp = member (op =) yp x
1.57 + val maxs =
1.58 + maxs |> filter (fn (_, max) => not (is_ancestor max newp))
1.59 + in
1.60 + if exists (is_ancestor new o fst) maxs then
1.61 + (maxs, news)
1.62 + else
1.63 + ((newp, new)
1.64 + :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
1.65 + news)
1.66 + end
1.67 + else
1.68 + (maxs, Graph.Keys.fold (insert_new seen)
1.69 + (Graph.imm_preds fact_G new) news))
1.70 + in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
1.71
1.72 (* Generate more suggestions than requested, because some might be thrown out
1.73 later for various reasons and "meshing" gives better results with some
1.74 @@ -602,7 +608,7 @@
1.75 let
1.76 val thy = Proof_Context.theory_of ctxt
1.77 val fact_G = #fact_G (mash_get ctxt)
1.78 - val parents = max_facts_in_graph fact_G facts
1.79 + val parents = maximal_in_graph fact_G facts
1.80 val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
1.81 val suggs =
1.82 if Graph.is_empty fact_G then []
1.83 @@ -618,7 +624,7 @@
1.84 (from :: parents, Graph.add_edge_acyclic (from, name) graph))
1.85 val graph = graph |> Graph.default_node (name, ())
1.86 val (parents, graph) = ([], graph) |> fold maybe_add_from parents
1.87 - val (deps, graph) = ([], graph) |> fold maybe_add_from deps
1.88 + val (deps, _) = ([], graph) |> fold maybe_add_from deps
1.89 in ((name, parents, feats, deps) :: adds, graph) end
1.90
1.91 val learn_timeout_slack = 2.0
1.92 @@ -647,7 +653,7 @@
1.93 val feats = features_of ctxt prover thy (Local, General) [t]
1.94 val deps = used_ths |> map nickname_of
1.95 val {fact_G} = mash_get ctxt
1.96 - val parents = max_facts_in_graph fact_G facts
1.97 + val parents = timeit (fn () => maximal_in_graph fact_G facts)
1.98 in
1.99 mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
1.100 end)
1.101 @@ -743,7 +749,7 @@
1.102 val ancestors =
1.103 old_facts
1.104 |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
1.105 - val parents = max_facts_in_graph fact_G ancestors
1.106 + val parents = maximal_in_graph fact_G ancestors
1.107 val (adds, (_, n, _, _)) =
1.108 ([], (parents, 0, next_commit_time (), false))
1.109 |> fold learn_new_fact new_facts
1.110 @@ -853,10 +859,13 @@
1.111 case fact_filter of
1.112 SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
1.113 | NONE =>
1.114 - if is_smt_prover ctxt prover then mepoN
1.115 - else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
1.116 - else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
1.117 - else mepoN
1.118 + if is_smt_prover ctxt prover then
1.119 + mepoN
1.120 + else if mash_could_suggest_facts () then
1.121 + (maybe_learn ();
1.122 + if mash_can_suggest_facts ctxt then meshN else mepoN)
1.123 + else
1.124 + mepoN
1.125 val add_ths = Attrib.eval_thms ctxt add
1.126 fun prepend_facts ths accepts =
1.127 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
2.3 @@ -64,8 +64,8 @@
2.4
2.5 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
2.6 timeout, expect, ...})
2.7 - mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
2.8 - name =
2.9 + mode minimize_command only learn
2.10 + {state, goal, subgoal, subgoal_count, facts} name =
2.11 let
2.12 val ctxt = Proof.context_of state
2.13 val hard_timeout = Time.+ (timeout, timeout)
2.14 @@ -93,9 +93,6 @@
2.15 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
2.16 " proof (of " ^ string_of_int (length facts) ^ "): ") "."
2.17 |> Output.urgent_message
2.18 - fun learn prover =
2.19 - mash_learn_proof ctxt params prover (prop_of goal)
2.20 - (map untranslated_fact facts)
2.21 fun really_go () =
2.22 problem
2.23 |> get_minimizing_prover ctxt mode learn name params minimize_command
2.24 @@ -188,7 +185,7 @@
2.25 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
2.26 val reserved = reserved_isar_keyword_table ()
2.27 val css = clasimpset_rule_table_of ctxt
2.28 - val facts =
2.29 + val all_facts =
2.30 nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
2.31 concl_t
2.32 val _ = () |> not blocking ? kill_provers
2.33 @@ -208,7 +205,9 @@
2.34 val problem =
2.35 {state = state, goal = goal, subgoal = i, subgoal_count = n,
2.36 facts = facts}
2.37 - val launch = launch_prover params mode minimize_command only
2.38 + fun learn prover =
2.39 + mash_learn_proof ctxt params prover (prop_of goal) all_facts
2.40 + val launch = launch_prover params mode minimize_command only learn
2.41 in
2.42 if mode = Auto_Try orelse mode = Try then
2.43 (unknownN, state)
2.44 @@ -232,7 +231,7 @@
2.45 provers
2.46 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
2.47 in
2.48 - facts
2.49 + all_facts
2.50 |> (case is_appropriate_prop of
2.51 SOME is_app => filter (is_app o prop_of o snd)
2.52 | NONE => I)