summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Mon, 06 Dec 2010 09:54:58 +0100 | |

changeset 40977 | 9140c5950494 |

parent 40965 | 54b6c9e1c157 |

child 40978 | 79d2ea0e1fdb |

[mq]: sledge_binary_minimizer

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Dec 05 14:02:16 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Dec 06 09:54:58 2010 +0100 @@ -2,7 +2,7 @@ Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen -Minimization of fact list for Metis using ATPs. +Minimization of fact list for Metis using external provers. *) signature SLEDGEHAMMER_MINIMIZE = @@ -62,16 +62,24 @@ facts = facts, only = true} val result as {outcome, used_facts, ...} = prover params (K "") problem in - Output.urgent_message (case outcome of - SOME failure => string_for_failure failure - | NONE => - if length used_facts = length facts then "Found proof." - else "Found proof with " ^ n_facts used_facts ^ "."); + Output.urgent_message + (case outcome of + SOME failure => string_for_failure failure + | NONE => + if length used_facts = length facts then "Found proof." + else "Found proof with " ^ n_facts used_facts ^ "."); result end (* minimalization of facts *) +(* The sublinear algorithm works well in almost all situations, except when the + external prover cannot return the list of used facts and hence returns all + facts as used. In that case, the binary algorithm is much more + appropriate. We can usually detect that situation just by looking at the + number of used facts reported by the prover. *) +val binary_threshold = 50 + fun filter_used_facts used = filter (member (op =) used o fst) fun sublinear_minimize _ [] p = p @@ -82,9 +90,35 @@ (filter_used_facts used_facts seen, result) | _ => sublinear_minimize test xs (x :: seen, result) -(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer - preprocessing time is included in the estimate below but isn't part of the - timeout. *) +fun binary_minimize test xs = + let + fun p xs = #outcome (test xs : prover_result) = NONE + fun split [] p = p + | split [h] (l, r) = (h :: l, r) + | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) + fun min _ [] = raise Empty + | min _ [s0] = [s0] + | min sup xs = + let val (l0, r0) = split xs ([], []) in + if p (sup @ l0) then + min sup l0 + else if p (sup @ r0) then + min sup r0 + else + let + val l = min (sup @ r0) l0 + val r = min (sup @ l) r0 + in l @ r end + end + val xs = + case min [] xs of + [x] => if p [] then [] else [x] + | xs => xs + in (xs, test xs) end + +(* Give the external prover some slack. The ATP gets further slack because the + Sledgehammer preprocessing time is included in the estimate below but isn't + part of the timeout. *) val fudge_msecs = 1000 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." @@ -95,7 +129,8 @@ val ctxt = Proof.context_of state val prover = get_prover ctxt false prover_name val msecs = Time.toMilliseconds timeout - val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".") + val _ = Output.urgent_message ("Sledgehammer minimize: " ^ + quote prover_name ^ ".") val {goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = @@ -112,9 +147,12 @@ val new_timeout = Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |> Time.fromMilliseconds + val facts = filter_used_facts used_facts facts val (min_thms, {message, ...}) = - sublinear_minimize (do_test new_timeout) - (filter_used_facts used_facts facts) ([], result) + if length facts >= binary_threshold then + binary_minimize (do_test new_timeout) facts + else + sublinear_minimize (do_test new_timeout) facts ([], result) val n = length min_thms val _ = Output.urgent_message (cat_lines ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ @@ -132,7 +170,7 @@ \can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ "\").") - | {message, ...} => (NONE, "ATP error: " ^ message)) + | {message, ...} => (NONE, "Prover error: " ^ message)) handle ERROR msg => (NONE, "Error: " ^ msg) end