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
     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) -> prover_problem ->
    67     prover_result
    68 
    69   val SledgehammerN : string
    70   val str_of_mode : mode -> string
    71   val smtN : string
    72   val overlord_file_location_of_prover : string -> string * string
    73   val proof_banner : mode -> string -> string
    74   val extract_proof_method : params -> proof_method -> string * (string * string list) list
    75   val is_proof_method : string -> bool
    76   val is_atp : theory -> string -> bool
    77   val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    78   val is_fact_chained : (('a * stature) * 'b) -> bool
    79   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    80     ((''a * stature) * 'b) list
    81   val play_one_line_proof : mode -> 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_Proof
    99 open ATP_Util
   100 open ATP_Systems
   101 open ATP_Problem
   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 (* Identifier that distinguishes Sledgehammer from other tools that could use
   109    "Async_Manager". *)
   110 val SledgehammerN = "Sledgehammer"
   111 
   112 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   113 
   114 fun str_of_mode Auto_Try = "Auto Try"
   115   | str_of_mode Try = "Try"
   116   | str_of_mode Normal = "Normal"
   117   | str_of_mode MaSh = "MaSh"
   118   | str_of_mode Auto_Minimize = "Auto_Minimize"
   119   | str_of_mode Minimize = "Minimize"
   120 
   121 val smtN = "smt"
   122 
   123 val proof_method_names = [metisN, smtN]
   124 val is_proof_method = member (op =) proof_method_names
   125 
   126 val is_atp = member (op =) o supported_atps
   127 
   128 type params =
   129   {debug : bool,
   130    verbose : bool,
   131    overlord : bool,
   132    spy : bool,
   133    blocking : bool,
   134    provers : string list,
   135    type_enc : string option,
   136    strict : bool,
   137    lam_trans : string option,
   138    uncurried_aliases : bool option,
   139    learn : bool,
   140    fact_filter : string option,
   141    max_facts : int option,
   142    fact_thresholds : real * real,
   143    max_mono_iters : int option,
   144    max_new_mono_instances : int option,
   145    isar_proofs : bool option,
   146    compress_isar : real,
   147    try0_isar : bool,
   148    smt_proofs : bool option,
   149    slice : bool,
   150    minimize : bool option,
   151    timeout : Time.time,
   152    preplay_timeout : Time.time,
   153    expect : string}
   154 
   155 type prover_problem =
   156   {comment : string,
   157    state : Proof.state,
   158    goal : thm,
   159    subgoal : int,
   160    subgoal_count : int,
   161    factss : (string * fact list) list}
   162 
   163 type prover_result =
   164   {outcome : atp_failure option,
   165    used_facts : (string * stature) list,
   166    used_from : fact list,
   167    run_time : Time.time,
   168    preplay : (proof_method * play_outcome) Lazy.lazy,
   169    message : proof_method * play_outcome -> string,
   170    message_tail : string}
   171 
   172 type prover =
   173   params -> ((string * string list) list -> string -> minimize_command)
   174   -> prover_problem -> prover_result
   175 
   176 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   177 
   178 fun proof_banner mode name =
   179   (case mode of
   180     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   181   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   182   | _ => "Try this")
   183 
   184 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   185   (if needs_full_types then
   186      [Metis_Method (SOME full_typesN, NONE),
   187       Metis_Method (SOME really_full_type_enc, NONE),
   188       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
   189       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
   190    else
   191      [Metis_Method (NONE, NONE),
   192       Metis_Method (SOME full_typesN, NONE),
   193       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
   194       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
   195   (if smt_proofs then [SMT2_Method] else [])
   196 
   197 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   198       (Metis_Method (type_enc', lam_trans')) =
   199     let
   200       val override_params =
   201         (if is_none type_enc' andalso is_none type_enc then []
   202          else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
   203         (if is_none lam_trans' andalso is_none lam_trans then []
   204          else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
   205     in (metisN, override_params) end
   206   | extract_proof_method _ SMT2_Method = (smtN, [])
   207 
   208 (* based on "Mirabelle.can_apply" and generalized *)
   209 fun timed_apply timeout tac state i =
   210   let
   211     val {context = ctxt, facts, goal} = Proof.goal state
   212     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   213   in
   214     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   215   end
   216 
   217 fun timed_proof_method timeout ths meth =
   218   timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
   219 
   220 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
   221 
   222 fun filter_used_facts keep_chained used =
   223   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
   224 
   225 fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
   226   let
   227     val ctxt = Proof.context_of state
   228 
   229     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   230   in
   231     if timeout = Time.zeroTime then
   232       (get_preferred meths, Play_Timed_Out Time.zeroTime)
   233     else
   234       let
   235         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
   236         val ths = pairs |> sort_wrt (fst o fst) |> map snd
   237         fun play [] [] = (get_preferred meths, Play_Failed)
   238           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
   239           | play timed_out (meth :: meths) =
   240             let
   241               val _ =
   242                 if verbose then
   243                   Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^
   244                     "\" for " ^ string_of_time timeout ^ "...")
   245                 else
   246                   ()
   247               val timer = Timer.startRealTimer ()
   248             in
   249               (case timed_proof_method timeout ths meth state i of
   250                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
   251               | _ => play timed_out meths)
   252             end
   253             handle TimeLimit.TimeOut => play (meth :: timed_out) meths
   254       in
   255         play [] meths
   256       end
   257   end
   258 
   259 val canonical_isar_supported_prover = eN
   260 val z3_newN = "z3_new"
   261 
   262 fun isar_supported_prover_of thy name =
   263   if is_atp thy name orelse name = z3_newN then name
   264   else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
   265   else name
   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 as Metis_Method _, 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       sort_strings (SMT2_Config.available_solvers_of ctxt)
   295       |> List.partition (String.isPrefix remote_prefix)
   296   in
   297     Output.urgent_message ("Supported provers: " ^ 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;