src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

bring ATPs and SMT solvers more in line with each other

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
    Author:     Philipp Meyer, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen

Minimization of fact list for Metis using ATPs.
*)

signature SLEDGEHAMMER_MINIMIZE =
sig
  type locality = Sledgehammer_Filter.locality
  type params = Sledgehammer.params

  val minimize_facts :
    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
    -> ((string * locality) * thm list) list option * string
  val run_minimize :
    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
end;

structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
struct

open ATP_Proof
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_Translate
open Sledgehammer

(* wrapper for calling external prover *)

fun string_for_failure Unprovable = "Unprovable."
  | string_for_failure TimedOut = "Timed out."
  | string_for_failure Interrupted = "Interrupted."
  | string_for_failure _ = "Unknown error."

fun n_facts names =
  let val n = length names in
    string_of_int n ^ " fact" ^ plural_s n ^
    (if n > 0 then
       ": " ^ (names |> map fst
                     |> sort_distinct string_ord |> space_implode " ")
     else
       "")
  end

fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
                 isar_shrink_factor, ...} : params) (prover : prover)
               explicit_apply timeout subgoal state axioms =
  let
    val _ =
      priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
    val params =
      {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
       provers = provers, full_types = full_types,
       explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
       max_relevant = NONE, isar_proof = isar_proof,
       isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
    val axioms =
      axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
    val {context = ctxt, goal, ...} = Proof.goal state
    val prover_problem =
      {state = state, goal = goal, subgoal = subgoal, axioms = axioms,
       only = true}
    val result as {outcome, used_axioms, ...} =
      prover params (K "") prover_problem
  in
    priority (case outcome of
                SOME failure => string_for_failure failure
              | NONE =>
                if length used_axioms = length axioms then "Found proof."
                else "Found proof with " ^ n_facts used_axioms ^ ".");
    result
  end

(* minimalization of thms *)

fun filter_used_axioms used = filter (member (op =) used o fst)

fun sublinear_minimize _ [] p = p
  | sublinear_minimize test (x :: xs) (seen, result) =
    case test (xs @ seen) of
      result as {outcome = NONE, used_axioms, ...} : prover_result =>
      sublinear_minimize test (filter_used_axioms used_axioms xs)
                         (filter_used_axioms used_axioms 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. *)
val fudge_msecs = 1000

fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
  | minimize_facts (params as {provers = prover_name :: _, timeout, ...})
                   i (_ : int) state axioms =
  let
    val thy = Proof.theory_of state
    val prover = get_prover thy false prover_name
    val msecs = Time.toMilliseconds timeout
    val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
    val {goal, ...} = Proof.goal state
    val (_, hyp_ts, concl_t) = strip_subgoal goal i
    val explicit_apply =
      not (forall (Meson.is_fol_term thy)
                  (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
    fun do_test timeout =
      test_facts params prover explicit_apply timeout i state
    val timer = Timer.startRealTimer ()
  in
    (case do_test timeout axioms of
       result as {outcome = NONE, used_axioms, ...} =>
       let
         val time = Timer.checkRealTimer timer
         val new_timeout =
           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
           |> Time.fromMilliseconds
         val (min_thms, {message, ...}) =
           sublinear_minimize (do_test new_timeout)
               (filter_used_axioms used_axioms axioms) ([], result)
         val n = length min_thms
         val _ = priority (cat_lines
           ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
               0 => ""
             | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
       in (SOME min_thms, message) end
     | {outcome = SOME TimedOut, ...} =>
       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
              \option (e.g., \"timeout = " ^
              string_of_int (10 + msecs div 1000) ^ " s\").")
     | {outcome = SOME UnknownError, ...} =>
       (* Failure sometimes mean timeout, unfortunately. *)
       (NONE, "Failure: No proof was found with the current time limit. You \
              \can increase the time limit using the \"timeout\" \
              \option (e.g., \"timeout = " ^
              string_of_int (10 + msecs div 1000) ^ " s\").")
     | {message, ...} => (NONE, "ATP error: " ^ message))
    handle ERROR msg => (NONE, "Error: " ^ msg)
  end

fun run_minimize params i refs state =
  let
    val ctxt = Proof.context_of state
    val reserved = reserved_isar_keyword_table ()
    val chained_ths = #facts (Proof.goal state)
    val axioms =
      maps (map (apsnd single)
            o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
  in
    case subgoal_count state of
      0 => priority "No subgoal!"
    | n =>
      (kill_provers ();
       priority (#2 (minimize_facts params i n state axioms)))
  end

end;