src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Thu Feb 13 13:16:17 2014 +0100 (2014-02-13 ago)
changeset 55453 0b070d098d1a
parent 55452 29ec8680e61f
child 55458 d3b72d260d4a
permissions -rw-r--r--
repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Generic prover abstraction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVER =
    10 sig
    11   type atp_failure = ATP_Proof.atp_failure
    12   type stature = ATP_Problem_Generate.stature
    13   type type_enc = ATP_Problem_Generate.type_enc
    14   type fact = Sledgehammer_Fact.fact
    15   type proof_method = Sledgehammer_Proof_Methods.proof_method
    16   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
    17   type minimize_command = Sledgehammer_Proof_Methods.minimize_command
    18 
    19   datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    20 
    21   type params =
    22     {debug : bool,
    23      verbose : bool,
    24      overlord : bool,
    25      spy : bool,
    26      blocking : bool,
    27      provers : string list,
    28      type_enc : string option,
    29      strict : bool,
    30      lam_trans : string option,
    31      uncurried_aliases : bool option,
    32      learn : bool,
    33      fact_filter : string option,
    34      max_facts : int option,
    35      fact_thresholds : real * real,
    36      max_mono_iters : int option,
    37      max_new_mono_instances : int option,
    38      isar_proofs : bool option,
    39      compress_isar : real,
    40      try0_isar : bool,
    41      smt_proofs : bool option,
    42      slice : bool,
    43      minimize : bool option,
    44      timeout : Time.time,
    45      preplay_timeout : Time.time,
    46      expect : string}
    47 
    48   type prover_problem =
    49     {comment : string,
    50      state : Proof.state,
    51      goal : thm,
    52      subgoal : int,
    53      subgoal_count : int,
    54      factss : (string * fact list) list}
    55 
    56   type prover_result =
    57     {outcome : atp_failure option,
    58      used_facts : (string * stature) list,
    59      used_from : fact list,
    60      run_time : Time.time,
    61      preplay : (proof_method * play_outcome) Lazy.lazy,
    62      message : proof_method * play_outcome -> string,
    63      message_tail : string}
    64 
    65   type prover =
    66     params -> ((string * string list) list -> string -> minimize_command)
    67     -> prover_problem -> prover_result
    68 
    69   val SledgehammerN : string
    70   val smtN : string
    71   val overlord_file_location_of_prover : string -> string * string
    72   val proof_banner : mode -> string -> string
    73   val extract_proof_method : params -> proof_method -> string * (string * string list) list
    74   val is_proof_method : string -> bool
    75   val is_atp : theory -> string -> bool
    76   val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    77   val is_fact_chained : (('a * stature) * 'b) -> bool
    78   val filter_used_facts :
    79     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    80     ((''a * stature) * 'b) list
    81   val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
    82     Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
    83   val remotify_atp_if_not_installed : theory -> string -> string option
    84   val isar_supported_prover_of : theory -> string -> string
    85   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    86     string -> proof_method * play_outcome -> 'a
    87   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    88     Proof.context
    89 
    90   val supported_provers : Proof.context -> unit
    91   val kill_provers : unit -> unit
    92   val running_provers : unit -> unit
    93   val messages : int option -> unit
    94 end;
    95 
    96 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
    97 struct
    98 
    99 open ATP_Util
   100 open ATP_Problem
   101 open ATP_Systems
   102 open ATP_Problem_Generate
   103 open ATP_Proof_Reconstruct
   104 open Metis_Tactic
   105 open Sledgehammer_Fact
   106 open Sledgehammer_Proof_Methods
   107 
   108 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   109 
   110 (* Identifier that distinguishes Sledgehammer from other tools that could use
   111    "Async_Manager". *)
   112 val SledgehammerN = "Sledgehammer"
   113 
   114 val smtN = "smt"
   115 
   116 val proof_method_names = [metisN, smtN]
   117 val is_proof_method = member (op =) proof_method_names
   118 
   119 val is_atp = member (op =) o supported_atps
   120 
   121 fun remotify_atp_if_not_installed thy name =
   122   if is_atp thy name then
   123     if String.isPrefix remote_prefix name orelse is_atp_installed thy name then
   124       SOME name
   125     else
   126       let val remote_name = remote_prefix ^ name in
   127         if is_atp thy remote_name then SOME remote_name else NONE
   128       end
   129   else
   130     SOME name
   131 
   132 type params =
   133   {debug : bool,
   134    verbose : bool,
   135    overlord : bool,
   136    spy : bool,
   137    blocking : bool,
   138    provers : string list,
   139    type_enc : string option,
   140    strict : bool,
   141    lam_trans : string option,
   142    uncurried_aliases : bool option,
   143    learn : bool,
   144    fact_filter : string option,
   145    max_facts : int option,
   146    fact_thresholds : real * real,
   147    max_mono_iters : int option,
   148    max_new_mono_instances : int option,
   149    isar_proofs : bool option,
   150    compress_isar : real,
   151    try0_isar : bool,
   152    smt_proofs : bool option,
   153    slice : bool,
   154    minimize : bool option,
   155    timeout : Time.time,
   156    preplay_timeout : Time.time,
   157    expect : string}
   158 
   159 type prover_problem =
   160   {comment : string,
   161    state : Proof.state,
   162    goal : thm,
   163    subgoal : int,
   164    subgoal_count : int,
   165    factss : (string * fact list) list}
   166 
   167 type prover_result =
   168   {outcome : atp_failure option,
   169    used_facts : (string * stature) list,
   170    used_from : fact list,
   171    run_time : Time.time,
   172    preplay : (proof_method * play_outcome) Lazy.lazy,
   173    message : proof_method * play_outcome -> string,
   174    message_tail : string}
   175 
   176 type prover =
   177   params -> ((string * string list) list -> string -> minimize_command)
   178   -> prover_problem -> prover_result
   179 
   180 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   181 
   182 fun proof_banner mode name =
   183   (case mode of
   184     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   185   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   186   | _ => "Try this")
   187 
   188 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   189   (if needs_full_types then
   190      [Metis_Method (SOME full_typesN, NONE),
   191       Metis_Method (SOME really_full_type_enc, NONE),
   192       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
   193       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
   194    else
   195      [Metis_Method (NONE, NONE),
   196       Metis_Method (SOME full_typesN, NONE),
   197       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
   198       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
   199   (if smt_proofs then [SMT_Method] else [])
   200 
   201 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   202       (Metis_Method (type_enc', lam_trans')) =
   203     let
   204       val override_params =
   205         (if is_none type_enc' andalso is_none type_enc then []
   206          else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
   207         (if is_none lam_trans' andalso is_none lam_trans then []
   208          else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
   209     in (metisN, override_params) end
   210   | extract_proof_method _ SMT_Method = (smtN, [])
   211 
   212 (* based on "Mirabelle.can_apply" and generalized *)
   213 fun timed_apply timeout tac state i =
   214   let
   215     val {context = ctxt, facts, goal} = Proof.goal state
   216     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   217   in
   218     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   219   end
   220 
   221 fun timed_proof_method debug timeout ths meth =
   222   timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
   223 
   224 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
   225 
   226 fun filter_used_facts keep_chained used =
   227   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
   228 
   229 fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   230   let
   231     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   232   in
   233     if timeout = Time.zeroTime then
   234       (get_preferred meths, Not_Played)
   235     else
   236       let
   237         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
   238         val ths = pairs |> sort_wrt (fst o fst) |> map snd
   239         fun play [] [] = (get_preferred meths, Play_Failed)
   240           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
   241           | play timed_out (meth :: meths) =
   242             let
   243               val _ =
   244                 if verbose then
   245                   Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
   246                     "\" for " ^ string_of_time timeout ^ "...")
   247                 else
   248                   ()
   249               val timer = Timer.startRealTimer ()
   250             in
   251               (case timed_proof_method debug timeout ths meth state i of
   252                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
   253               | _ => play timed_out meths)
   254             end
   255             handle TimeLimit.TimeOut => play (meth :: timed_out) meths
   256       in
   257         play [] meths
   258       end
   259   end
   260 
   261 val canonical_isar_supported_prover = eN
   262 
   263 fun isar_supported_prover_of thy name =
   264   if is_atp thy name then name
   265   else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
   266 
   267 (* FIXME: See the analogous logic in the function "maybe_minimize" in
   268    "sledgehammer_prover_minimize.ML". *)
   269 fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
   270   let
   271     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
   272     val (min_name, override_params) =
   273       (case preplay of
   274         (meth, Played _) =>
   275         if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
   276       | _ => (maybe_isar_name, []))
   277   in minimize_command override_params min_name end
   278 
   279 val max_fact_instances = 10 (* FUDGE *)
   280 
   281 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   282   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   283   #> Config.put Monomorph.max_new_instances
   284        (max_new_instances |> the_default best_max_new_instances)
   285   #> Config.put Monomorph.max_thm_instances max_fact_instances
   286 
   287 fun supported_provers ctxt =
   288   let
   289     val thy = Proof_Context.theory_of ctxt
   290     val (remote_provers, local_provers) =
   291       proof_method_names @
   292       sort_strings (supported_atps thy) @
   293       sort_strings (SMT_Solver.available_solvers_of ctxt)
   294       |> List.partition (String.isPrefix remote_prefix)
   295   in
   296     Output.urgent_message ("Supported provers: " ^
   297                            commas (local_provers @ remote_provers) ^ ".")
   298   end
   299 
   300 fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   301 fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   302 val messages = Async_Manager.thread_messages SledgehammerN "prover"
   303 
   304 end;