src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13 ago)
changeset 56081 72fad75baf7e
parent 55475 b8ebbcc5e49a
child 56084 75c154e9f650
permissions -rw-r--r--
integrate SMT2 with Sledgehammer
     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 isar_supported_prover_of : theory -> string -> string
    84   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    85     string -> proof_method * play_outcome -> 'a
    86   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    87     Proof.context
    88 
    89   val supported_provers : Proof.context -> unit
    90   val kill_provers : unit -> unit
    91   val running_provers : unit -> unit
    92   val messages : int option -> unit
    93 end;
    94 
    95 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
    96 struct
    97 
    98 open ATP_Util
    99 open ATP_Problem
   100 open ATP_Systems
   101 open ATP_Problem_Generate
   102 open ATP_Proof_Reconstruct
   103 open Metis_Tactic
   104 open Sledgehammer_Fact
   105 open Sledgehammer_Proof_Methods
   106 
   107 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   108 
   109 (* Identifier that distinguishes Sledgehammer from other tools that could use
   110    "Async_Manager". *)
   111 val SledgehammerN = "Sledgehammer"
   112 
   113 val smtN = "smt"
   114 
   115 val proof_method_names = [metisN, smtN]
   116 val is_proof_method = member (op =) proof_method_names
   117 
   118 val is_atp = member (op =) o supported_atps
   119 
   120 type params =
   121   {debug : bool,
   122    verbose : bool,
   123    overlord : bool,
   124    spy : bool,
   125    blocking : bool,
   126    provers : string list,
   127    type_enc : string option,
   128    strict : bool,
   129    lam_trans : string option,
   130    uncurried_aliases : bool option,
   131    learn : bool,
   132    fact_filter : string option,
   133    max_facts : int option,
   134    fact_thresholds : real * real,
   135    max_mono_iters : int option,
   136    max_new_mono_instances : int option,
   137    isar_proofs : bool option,
   138    compress_isar : real,
   139    try0_isar : bool,
   140    smt_proofs : bool option,
   141    slice : bool,
   142    minimize : bool option,
   143    timeout : Time.time,
   144    preplay_timeout : Time.time,
   145    expect : string}
   146 
   147 type prover_problem =
   148   {comment : string,
   149    state : Proof.state,
   150    goal : thm,
   151    subgoal : int,
   152    subgoal_count : int,
   153    factss : (string * fact list) list}
   154 
   155 type prover_result =
   156   {outcome : atp_failure option,
   157    used_facts : (string * stature) list,
   158    used_from : fact list,
   159    run_time : Time.time,
   160    preplay : (proof_method * play_outcome) Lazy.lazy,
   161    message : proof_method * play_outcome -> string,
   162    message_tail : string}
   163 
   164 type prover =
   165   params -> ((string * string list) list -> string -> minimize_command)
   166   -> prover_problem -> prover_result
   167 
   168 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   169 
   170 fun proof_banner mode name =
   171   (case mode of
   172     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   173   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   174   | _ => "Try this")
   175 
   176 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   177   (if needs_full_types then
   178      [Metis_Method (SOME full_typesN, NONE),
   179       Metis_Method (SOME really_full_type_enc, NONE),
   180       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
   181       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
   182    else
   183      [Metis_Method (NONE, NONE),
   184       Metis_Method (SOME full_typesN, NONE),
   185       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
   186       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
   187   (if smt_proofs then [SMT2_Method] else [])
   188 
   189 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   190       (Metis_Method (type_enc', lam_trans')) =
   191     let
   192       val override_params =
   193         (if is_none type_enc' andalso is_none type_enc then []
   194          else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
   195         (if is_none lam_trans' andalso is_none lam_trans then []
   196          else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
   197     in (metisN, override_params) end
   198   | extract_proof_method _ SMT2_Method = (smtN, [])
   199 
   200 (* based on "Mirabelle.can_apply" and generalized *)
   201 fun timed_apply timeout tac state i =
   202   let
   203     val {context = ctxt, facts, goal} = Proof.goal state
   204     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   205   in
   206     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   207   end
   208 
   209 fun timed_proof_method debug timeout ths meth =
   210   timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
   211 
   212 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
   213 
   214 fun filter_used_facts keep_chained used =
   215   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
   216 
   217 fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   218   let
   219     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   220   in
   221     if timeout = Time.zeroTime then
   222       (get_preferred meths, Not_Played)
   223     else
   224       let
   225         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
   226         val ths = pairs |> sort_wrt (fst o fst) |> map snd
   227         fun play [] [] = (get_preferred meths, Play_Failed)
   228           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
   229           | play timed_out (meth :: meths) =
   230             let
   231               val _ =
   232                 if verbose then
   233                   Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
   234                     "\" for " ^ string_of_time timeout ^ "...")
   235                 else
   236                   ()
   237               val timer = Timer.startRealTimer ()
   238             in
   239               (case timed_proof_method debug timeout ths meth state i of
   240                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
   241               | _ => play timed_out meths)
   242             end
   243             handle TimeLimit.TimeOut => play (meth :: timed_out) meths
   244       in
   245         play [] meths
   246       end
   247   end
   248 
   249 val canonical_isar_supported_prover = eN
   250 
   251 fun isar_supported_prover_of thy name =
   252   if is_atp thy name then name
   253   else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
   254   else name
   255 
   256 (* FIXME: See the analogous logic in the function "maybe_minimize" in
   257    "sledgehammer_prover_minimize.ML". *)
   258 fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
   259   let
   260     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
   261     val (min_name, override_params) =
   262       (case preplay of
   263         (meth, Played _) =>
   264         if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
   265       | _ => (maybe_isar_name, []))
   266   in minimize_command override_params min_name end
   267 
   268 val max_fact_instances = 10 (* FUDGE *)
   269 
   270 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   271   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   272   #> Config.put Monomorph.max_new_instances
   273        (max_new_instances |> the_default best_max_new_instances)
   274   #> Config.put Monomorph.max_thm_instances max_fact_instances
   275 
   276 fun supported_provers ctxt =
   277   let
   278     val thy = Proof_Context.theory_of ctxt
   279     val (remote_provers, local_provers) =
   280       proof_method_names @
   281       sort_strings (supported_atps thy) @
   282       sort_strings (SMT_Solver.available_solvers_of ctxt) @
   283       sort_strings (SMT2_Solver.available_solvers_of ctxt)
   284       |> List.partition (String.isPrefix remote_prefix)
   285   in
   286     Output.urgent_message ("Supported provers: " ^
   287                            commas (local_provers @ remote_provers) ^ ".")
   288   end
   289 
   290 fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   291 fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   292 val messages = Async_Manager.thread_messages SledgehammerN "prover"
   293 
   294 end;