src/HOL/Tools/ATP_Manager/atp_manager.ML
author blanchet
Fri Jun 25 18:05:36 2010 +0200 (2010-06-25 ago)
changeset 37583 9ce2451647d5
parent 37581 03edc498db6f
child 37584 2e289dc13615
permissions -rw-r--r--
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
wenzelm@32327
     1
(*  Title:      HOL/Tools/ATP_Manager/atp_manager.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
wenzelm@32996
     6
Central manager component for ATP threads.
wenzelm@28477
     7
*)
wenzelm@28477
     8
wenzelm@28477
     9
signature ATP_MANAGER =
wenzelm@28477
    10
sig
blanchet@37574
    11
  type cnf_thm = Clausifier.cnf_thm
blanchet@37578
    12
  type name_pool = Metis_Clauses.name_pool
blanchet@35969
    13
  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
blanchet@36281
    14
  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
blanchet@35969
    15
  type params =
blanchet@35969
    16
    {debug: bool,
blanchet@35969
    17
     verbose: bool,
blanchet@36143
    18
     overlord: bool,
blanchet@35969
    19
     atps: string list,
blanchet@35969
    20
     full_types: bool,
blanchet@36235
    21
     explicit_apply: bool,
blanchet@35969
    22
     relevance_threshold: real,
blanchet@36922
    23
     relevance_convergence: real,
blanchet@36220
    24
     theory_relevant: bool option,
blanchet@36922
    25
     defs_relevant: bool,
blanchet@35969
    26
     isar_proof: bool,
blanchet@36924
    27
     isar_shrink_factor: int,
blanchet@35969
    28
     timeout: Time.time,
blanchet@35969
    29
     minimize_timeout: Time.time}
blanchet@35867
    30
  type problem =
blanchet@35969
    31
    {subgoal: int,
blanchet@35969
    32
     goal: Proof.context * (thm list * thm),
blanchet@35969
    33
     relevance_override: relevance_override,
blanchet@37500
    34
     axiom_clauses: cnf_thm list option,
blanchet@37500
    35
     filtered_clauses: cnf_thm list option}
blanchet@36370
    36
  datatype failure =
blanchet@37413
    37
    Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
blanchet@37413
    38
    MalformedInput | MalformedOutput | UnknownError
blanchet@35867
    39
  type prover_result =
blanchet@36370
    40
    {outcome: failure option,
blanchet@35969
    41
     message: string,
blanchet@36393
    42
     pool: name_pool option,
blanchet@35969
    43
     relevant_thm_names: string list,
blanchet@35969
    44
     atp_run_time_in_msecs: int,
blanchet@36369
    45
     output: string,
blanchet@35969
    46
     proof: string,
blanchet@35969
    47
     internal_thm_names: string Vector.vector,
blanchet@36400
    48
     conjecture_shape: int list list,
blanchet@37500
    49
     filtered_clauses: cnf_thm list}
blanchet@36281
    50
  type prover =
blanchet@36281
    51
    params -> minimize_command -> Time.time -> problem -> prover_result
blanchet@35867
    52
blanchet@35969
    53
  val kill_atps: unit -> unit
blanchet@35969
    54
  val running_atps: unit -> unit
wenzelm@29112
    55
  val messages: int option -> unit
blanchet@35867
    56
  val add_prover: string * prover -> theory -> theory
blanchet@36379
    57
  val get_prover: theory -> string -> prover
blanchet@35969
    58
  val available_atps: theory -> unit
blanchet@36373
    59
  val start_prover_thread:
blanchet@36482
    60
    params -> Time.time -> Time.time -> int -> int -> relevance_override
blanchet@36373
    61
    -> (string -> minimize_command) -> Proof.state -> string -> unit
wenzelm@28477
    62
end;
wenzelm@28477
    63
blanchet@35865
    64
structure ATP_Manager : ATP_MANAGER =
wenzelm@28477
    65
struct
wenzelm@28477
    66
blanchet@37578
    67
open Metis_Clauses
blanchet@36063
    68
open Sledgehammer_Fact_Filter
blanchet@36063
    69
open Sledgehammer_Proof_Reconstruct
blanchet@37583
    70
open Async_Manager
blanchet@37583
    71
blanchet@37583
    72
(** The Sledgehammer **)
blanchet@37583
    73
blanchet@37583
    74
fun kill_atps () = kill_threads "ATPs"
blanchet@37583
    75
fun running_atps () = running_threads "ATPs"
blanchet@37583
    76
val messages = thread_messages "ATP"
blanchet@35969
    77
blanchet@36281
    78
(** problems, results, provers, etc. **)
blanchet@35969
    79
blanchet@35969
    80
type params =
blanchet@35969
    81
  {debug: bool,
blanchet@35969
    82
   verbose: bool,
blanchet@36143
    83
   overlord: bool,
blanchet@35969
    84
   atps: string list,
blanchet@35969
    85
   full_types: bool,
blanchet@36235
    86
   explicit_apply: bool,
blanchet@35969
    87
   relevance_threshold: real,
blanchet@36922
    88
   relevance_convergence: real,
blanchet@36220
    89
   theory_relevant: bool option,
blanchet@36922
    90
   defs_relevant: bool,
blanchet@35969
    91
   isar_proof: bool,
blanchet@36924
    92
   isar_shrink_factor: int,
blanchet@35969
    93
   timeout: Time.time,
blanchet@35969
    94
   minimize_timeout: Time.time}
blanchet@35867
    95
blanchet@35867
    96
type problem =
blanchet@35969
    97
  {subgoal: int,
blanchet@35969
    98
   goal: Proof.context * (thm list * thm),
blanchet@35969
    99
   relevance_override: relevance_override,
blanchet@37500
   100
   axiom_clauses: cnf_thm list option,
blanchet@37500
   101
   filtered_clauses: cnf_thm list option}
blanchet@35867
   102
blanchet@36370
   103
datatype failure =
blanchet@37413
   104
  Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
blanchet@37413
   105
  MalformedInput | MalformedOutput | UnknownError
blanchet@36370
   106
blanchet@35867
   107
type prover_result =
blanchet@36370
   108
  {outcome: failure option,
blanchet@35969
   109
   message: string,
blanchet@36393
   110
   pool: name_pool option,
blanchet@35969
   111
   relevant_thm_names: string list,
blanchet@35969
   112
   atp_run_time_in_msecs: int,
blanchet@36369
   113
   output: string,
blanchet@35969
   114
   proof: string,
blanchet@35969
   115
   internal_thm_names: string Vector.vector,
blanchet@36400
   116
   conjecture_shape: int list list,
blanchet@37500
   117
   filtered_clauses: cnf_thm list}
blanchet@35867
   118
blanchet@36281
   119
type prover =
blanchet@36281
   120
  params -> minimize_command -> Time.time -> problem -> prover_result
blanchet@35867
   121
wenzelm@28582
   122
(* named provers *)
wenzelm@28484
   123
blanchet@36379
   124
structure Data = Theory_Data
wenzelm@28582
   125
(
blanchet@35867
   126
  type T = (prover * stamp) Symtab.table;
wenzelm@32938
   127
  val empty = Symtab.empty;
wenzelm@32938
   128
  val extend = I;
wenzelm@33522
   129
  fun merge data : T = Symtab.merge (eq_snd op =) data
blanchet@37580
   130
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   131
);
wenzelm@28484
   132
boehmes@32864
   133
fun add_prover (name, prover) thy =
blanchet@36379
   134
  Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
blanchet@37580
   135
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   136
wenzelm@32995
   137
fun get_prover thy name =
blanchet@37580
   138
  the (Symtab.lookup (Data.get thy) name) |> fst
blanchet@37580
   139
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
wenzelm@32995
   140
blanchet@36229
   141
fun available_atps thy =
blanchet@36229
   142
  priority ("Available ATPs: " ^
blanchet@36379
   143
            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
wenzelm@28571
   144
wenzelm@28586
   145
wenzelm@28595
   146
(* start prover thread *)
wenzelm@28484
   147
blanchet@37581
   148
fun start_prover_thread (params as {verbose, full_types, timeout, ...})
blanchet@37581
   149
                        birth_time death_time i n relevance_override
blanchet@37581
   150
                        minimize_command proof_state name =
blanchet@36379
   151
  let
blanchet@36379
   152
    val prover = get_prover (Proof.theory_of proof_state) name
blanchet@36379
   153
    val {context = ctxt, facts, goal} = Proof.goal proof_state;
blanchet@36379
   154
    val desc =
blanchet@36379
   155
      "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
blanchet@36392
   156
      Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
blanchet@36379
   157
    val _ = Toplevel.thread true (fn () =>
wenzelm@28595
   158
      let
blanchet@37583
   159
        val _ = register "Sledgehammer" verbose birth_time death_time
blanchet@37583
   160
                         (Thread.self (), desc)
blanchet@36379
   161
        val problem =
blanchet@36379
   162
          {subgoal = i, goal = (ctxt, (facts, goal)),
blanchet@36379
   163
           relevance_override = relevance_override, axiom_clauses = NONE,
blanchet@36379
   164
           filtered_clauses = NONE}
blanchet@36379
   165
        val message =
blanchet@36379
   166
          #message (prover params (minimize_command name) timeout problem)
blanchet@37506
   167
          handle TRIVIAL () => metis_line full_types i n []
blanchet@36383
   168
               | ERROR message => "Error: " ^ message ^ "\n"
blanchet@37581
   169
        val _ = unregister verbose message (Thread.self ());
blanchet@36379
   170
      in () end)
blanchet@36379
   171
  in () end
wenzelm@28582
   172
wenzelm@28582
   173
end;