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