src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
author blanchet
Sun May 01 18:37:23 2011 +0200 (2011-05-01)
changeset 42520 d1f7c4a01dbe
parent 42444 8e5438dc70bb
child 42579 2552c09b1a72
permissions -rw-r--r--
renamings
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     2     Author:     Philipp Meyer, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Minimization of fact list for Metis using external provers.
     6 *)
     7 
     8 signature SLEDGEHAMMER_MINIMIZE =
     9 sig
    10   type locality = Sledgehammer_Filter.locality
    11   type params = Sledgehammer_Provers.params
    12 
    13   val binary_min_facts : int Unsynchronized.ref
    14   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
    15   val minimize_facts :
    16     string -> params -> bool option -> bool -> int -> int -> Proof.state
    17     -> ((string * locality) * thm list) list
    18     -> ((string * locality) * thm list) list option * string
    19   val run_minimize :
    20     params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
    21 end;
    22 
    23 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
    24 struct
    25 
    26 open ATP_Proof
    27 open Sledgehammer_Util
    28 open Sledgehammer_Filter
    29 open Sledgehammer_Provers
    30 
    31 (* wrapper for calling external prover *)
    32 
    33 fun n_facts names =
    34   let val n = length names in
    35     string_of_int n ^ " fact" ^ plural_s n ^
    36     (if n > 0 then
    37        ": " ^ (names |> map fst
    38                      |> sort_distinct string_ord |> space_implode " ")
    39      else
    40        "")
    41   end
    42 
    43 fun print silent f = if silent then () else Output.urgent_message (f ())
    44 
    45 fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
    46                  type_sys, isar_proof, isar_shrink_factor, ...} : params)
    47         explicit_apply_opt silent (prover : prover) timeout i n state facts =
    48   let
    49     val thy = Proof.theory_of state
    50     val _ =
    51       print silent (fn () =>
    52           "Testing " ^ n_facts (map fst facts) ^
    53           (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
    54           else "") ^ "...")
    55     val {goal, ...} = Proof.goal state
    56     val explicit_apply =
    57       case explicit_apply_opt of
    58         SOME explicit_apply => explicit_apply
    59       | NONE =>
    60         let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
    61           not (forall (Meson.is_fol_term thy)
    62                       (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
    63         end
    64     val params =
    65       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    66        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    67        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    68        monomorphize = false, monomorphize_limit = monomorphize_limit,
    69        isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    70        slicing = false, timeout = timeout, expect = ""}
    71     val facts =
    72       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    73     val problem =
    74       {state = state, goal = goal, subgoal = i, subgoal_count = n,
    75        facts = facts, smt_filter = NONE}
    76     val result as {outcome, used_facts, ...} = prover params (K "") problem
    77   in
    78     print silent (fn () =>
    79         case outcome of
    80           SOME failure => string_for_failure failure
    81         | NONE => if length used_facts = length facts then "Found proof."
    82                   else "Found proof with " ^ n_facts used_facts ^ ".");
    83     result
    84   end
    85 
    86 (* minimalization of facts *)
    87 
    88 (* The sublinear algorithm works well in almost all situations, except when the
    89    external prover cannot return the list of used facts and hence returns all
    90    facts as used. In that case, the binary algorithm is much more appropriate.
    91    We can usually detect the situation by looking at the number of used facts
    92    reported by the prover. *)
    93 val binary_min_facts = Unsynchronized.ref 20
    94 
    95 fun filter_used_facts used = filter (member (op =) used o fst)
    96 
    97 fun sublinear_minimize _ [] p = p
    98   | sublinear_minimize test (x :: xs) (seen, result) =
    99     case test (xs @ seen) of
   100       result as {outcome = NONE, used_facts, ...} : prover_result =>
   101       sublinear_minimize test (filter_used_facts used_facts xs)
   102                          (filter_used_facts used_facts seen, result)
   103     | _ => sublinear_minimize test xs (x :: seen, result)
   104 
   105 fun binary_minimize test xs =
   106   let
   107     fun p xs = #outcome (test xs : prover_result) = NONE
   108     fun split [] p = p
   109       | split [h] (l, r) = (h :: l, r)
   110       | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
   111     fun min _ _ [] = raise Empty
   112       | min _ _ [s0] = [s0]
   113       | min depth sup xs =
   114         let
   115 (*
   116           val _ = warning (replicate_string depth " " ^ "{" ^ ("  " ^
   117                            n_facts (map fst sup) ^ " and " ^
   118                            n_facts (map fst xs)))
   119 *)
   120           val (l0, r0) = split xs ([], [])
   121         in
   122           if p (sup @ l0) then
   123             min (depth + 1) sup l0
   124           else if p (sup @ r0) then
   125             min (depth + 1) sup r0
   126           else
   127             let
   128               val l = min (depth + 1) (sup @ r0) l0
   129               val r = min (depth + 1) (sup @ l) r0
   130             in l @ r end
   131         end
   132 (*
   133         |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
   134 *)
   135     val xs =
   136       case min 0 [] xs of
   137         [x] => if p [] then [] else [x]
   138       | xs => xs
   139   in (xs, test xs) end
   140 
   141 (* Give the external prover some slack. The ATP gets further slack because the
   142    Sledgehammer preprocessing time is included in the estimate below but isn't
   143    part of the timeout. *)
   144 val slack_msecs = 200
   145 
   146 fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
   147                    silent i n state facts =
   148   let
   149     val ctxt = Proof.context_of state
   150     val prover = get_prover ctxt false prover_name
   151     val msecs = Time.toMilliseconds timeout
   152     val _ = print silent (fn () => "Sledgehammer minimize: " ^
   153                                    quote prover_name ^ ".")
   154     fun do_test timeout =
   155       test_facts params explicit_apply_opt silent prover timeout i n state
   156     val timer = Timer.startRealTimer ()
   157   in
   158     (case do_test timeout facts of
   159        result as {outcome = NONE, used_facts, ...} =>
   160        let
   161          val time = Timer.checkRealTimer timer
   162          val new_timeout =
   163            Int.min (msecs, Time.toMilliseconds time + slack_msecs)
   164            |> Time.fromMilliseconds
   165          val facts = filter_used_facts used_facts facts
   166          val (min_thms, {message, ...}) =
   167            if length facts >= !binary_min_facts then
   168              binary_minimize (do_test new_timeout) facts
   169            else
   170              sublinear_minimize (do_test new_timeout) facts ([], result)
   171          val n = length min_thms
   172          val _ = print silent (fn () => cat_lines
   173            ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
   174             (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
   175                0 => ""
   176              | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
   177        in (SOME min_thms, message) end
   178      | {outcome = SOME TimedOut, ...} =>
   179        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   180               \option (e.g., \"timeout = " ^
   181               string_of_int (10 + msecs div 1000) ^ "\").")
   182      | {message, ...} => (NONE, "Prover error: " ^ message))
   183     handle ERROR msg => (NONE, "Error: " ^ msg)
   184   end
   185 
   186 fun run_minimize (params as {provers, ...}) i refs state =
   187   let
   188     val ctxt = Proof.context_of state
   189     val reserved = reserved_isar_keyword_table ()
   190     val chained_ths = #facts (Proof.goal state)
   191     val facts =
   192       refs
   193       |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
   194   in
   195     case subgoal_count state of
   196       0 => Output.urgent_message "No subgoal!"
   197     | n => case provers of
   198              [] => error "No prover is set."
   199            | prover :: _ =>
   200              (kill_provers ();
   201               minimize_facts prover params NONE false i n state facts
   202               |> #2 |> Output.urgent_message)
   203   end
   204 
   205 end;