# HG changeset patch # User blanchet # Date 1344009395 -7200 # Node ID cdcdb0547f29bed10547d106f769cccd31199be1 # Parent 5d63c23b4042b5d221df8129d4e2abaff91ef733 remember ATP flops to avoid repeating them too quickly diff -r 5d63c23b4042 -r cdcdb0547f29 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200 @@ -133,11 +133,23 @@ val unescape_metas = space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta +datatype proof_kind = Isar_Proof | ATP_Proof | Isar_Proof_wegen_ATP_Flop + +fun str_of_proof_kind Isar_Proof = "i" + | str_of_proof_kind ATP_Proof = "a" + | str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x" + +fun proof_kind_of_str "i" = Isar_Proof + | proof_kind_of_str "a" = ATP_Proof + | proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop + fun extract_node line = case space_explode ":" line of [head, parents] => (case space_explode " " head of - [tag, name] => SOME (unescape_meta name, unescape_metas parents, tag = "a") + [kind, name] => + SOME (unescape_meta name, unescape_metas parents, + try proof_kind_of_str kind |> the_default Isar_Proof) | _ => NONE) | _ => NONE @@ -501,9 +513,9 @@ (*** High-level communication with MaSh ***) (* FIXME: Here a "Graph.update_node" function would be useful *) -fun update_fact_graph_node (name, atp) = - Graph.default_node (name, false) - #> atp ? Graph.map_node name (K atp) +fun update_fact_graph_node (name, kind) = + Graph.default_node (name, Isar_Proof) + #> kind <> Isar_Proof ? Graph.map_node name (K kind) fun try_graph ctxt when def f = f () @@ -547,13 +559,13 @@ SOME (version' :: node_lines) => let fun add_edge_to name parent = - Graph.default_node (parent, false) + Graph.default_node (parent, Isar_Proof) #> Graph.add_edge (parent, name) fun add_node line = case extract_node line of NONE => I (* shouldn't happen *) - | SOME (name, parents, atp) => - update_fact_graph_node (name, atp) + | SOME (name, parents, kind) => + update_fact_graph_node (name, kind) #> fold (add_edge_to name) parents val fact_G = try_graph ctxt "loading state" Graph.empty (fn () => @@ -568,11 +580,11 @@ fun save ctxt {fact_G} = let - fun str_of_entry (name, parents, atp) = - (if atp then "a" else "i") ^ " " ^ escape_meta name ^ ": " ^ + fun str_of_entry (name, parents, kind) = + str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "\n" - fun append_entry (name, (atp, (parents, _))) = - cons (name, Graph.Keys.dest parents, atp) + fun append_entry (name, (kind, (parents, _))) = + cons (name, Graph.Keys.dest parents, kind) val entries = [] |> Graph.fold append_entry fact_G in write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ()); @@ -681,7 +693,7 @@ fun maybe_add_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) - val graph = graph |> Graph.default_node (name, false) + val graph = graph |> Graph.default_node (name, Isar_Proof) val (parents, graph) = ([], graph) |> fold maybe_add_from parents val (deps, _) = ([], graph) |> fold maybe_add_from deps in ((name, parents, feats, deps) :: adds, graph) end @@ -691,10 +703,13 @@ fun maybe_rep_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) - val graph = graph |> update_fact_graph_node (name, true) + val graph = graph |> update_fact_graph_node (name, ATP_Proof) val (deps, _) = ([], graph) |> fold maybe_rep_from deps in ((name, deps) :: reps, graph) end +fun flop_wrt_fact_graph name = + update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop) + val learn_timeout_slack = 2.0 fun launch_thread timeout task = @@ -766,24 +781,25 @@ |> (fn (false, _) => NONE | (true, deps) => deps) else isar_dependencies_of all_names th - fun do_commit [] [] state = state - | do_commit adds reps {fact_G} = + fun do_commit [] [] [] state = state + | do_commit adds reps flops {fact_G} = let val (adds, fact_G) = ([], fact_G) |> fold (add_wrt_fact_graph ctxt) adds val (reps, fact_G) = ([], fact_G) |> fold (reprove_wrt_fact_graph ctxt) reps + val fact_G = fact_G |> fold flop_wrt_fact_graph flops in mash_ADD ctxt overlord (rev adds); mash_REPROVE ctxt overlord reps; {fact_G = fact_G} end - fun commit last adds reps = + fun commit last adds reps flops = (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else (); - mash_map ctxt (do_commit (rev adds) reps); + mash_map ctxt (do_commit (rev adds) reps flops); if not last andalso auto_level = 0 then let val num_proofs = length adds + length reps in "Learned " ^ string_of_int num_proofs ^ " " ^ @@ -806,7 +822,7 @@ val adds = (name, parents, feats, deps) :: adds val (adds, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then - (commit false adds []; ([], next_commit_time ())) + (commit false adds [] []; ([], next_commit_time ())) else (adds, next_commit) val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) @@ -825,35 +841,38 @@ val (adds, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) |> fold learn_new_fact new_facts - in commit true adds []; n end + in commit true adds [] []; n end fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum | relearn_old_fact ((_, (_, status)), th) - (reps, (n, next_commit, _)) = + ((reps, flops), (n, next_commit, _)) = let val name = nickname_of th - val (n, reps) = + val (n, reps, flops) = case deps_of status th of - SOME deps => (n + 1, (name, deps) :: reps) - | NONE => (n, reps) - val (reps, next_commit) = + SOME deps => (n + 1, (name, deps) :: reps, flops) + | NONE => (n, reps, name :: flops) + val (reps, flops, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then - (commit false [] reps; ([], next_commit_time ())) + (commit false [] reps flops; ([], [], next_commit_time ())) else - (reps, next_commit) + (reps, flops, next_commit) val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) - in (reps, (n, next_commit, timed_out)) end + in ((reps, flops), (n, next_commit, timed_out)) end val n = if not atp orelse null old_facts then n else let val max_isar = 1000 * max_dependencies - fun has_atp_proof th = + fun kind_of_proof th = try (Graph.get_node fact_G) (nickname_of th) - |> the_default false + |> the_default Isar_Proof fun priority_of (_, th) = random_range 0 max_isar - + (if has_atp_proof th then max_isar else 0) + + (case kind_of_proof th of + Isar_Proof => 0 + | ATP_Proof => 2 * max_isar + | Isar_Proof_wegen_ATP_Flop => max_isar) - 500 * (th |> isar_dependencies_of all_names |> Option.map length |> the_default max_dependencies) @@ -861,10 +880,10 @@ old_facts |> map (`priority_of) |> sort (int_ord o pairself fst) |> map snd - val (reps, (n, _, _)) = - ([], (n, next_commit_time (), false)) + val ((reps, flops), (n, _, _)) = + (([], []), (n, next_commit_time (), false)) |> fold relearn_old_fact old_facts - in commit true [] reps; n end + in commit true [] reps flops; n end in if verbose orelse auto_level < 2 then "Learned " ^ string_of_int n ^ " nontrivial " ^