src/HOL/Tools/ATP_Manager/atp_manager.ML
author blanchet
Fri Jun 25 23:35:14 2010 +0200 (2010-06-25 ago)
changeset 37585 c2ed8112ce57
parent 37584 2e289dc13615
child 37621 3e78dbf7a382
permissions -rw-r--r--
multiplexing
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@37584
    59
  val start_prover_thread :
blanchet@37584
    60
    params -> int -> int -> relevance_override -> (string -> minimize_command)
blanchet@37584
    61
    -> 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
blanchet@37583
    71
(** The Sledgehammer **)
blanchet@37583
    72
blanchet@37585
    73
val das_Tool = "Sledgehammer"
blanchet@37585
    74
blanchet@37585
    75
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
blanchet@37585
    76
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
blanchet@37585
    77
val messages = Async_Manager.thread_messages das_Tool "ATP"
blanchet@35969
    78
blanchet@36281
    79
(** problems, results, provers, etc. **)
blanchet@35969
    80
blanchet@35969
    81
type params =
blanchet@35969
    82
  {debug: bool,
blanchet@35969
    83
   verbose: bool,
blanchet@36143
    84
   overlord: bool,
blanchet@35969
    85
   atps: string list,
blanchet@35969
    86
   full_types: bool,
blanchet@36235
    87
   explicit_apply: bool,
blanchet@35969
    88
   relevance_threshold: real,
blanchet@36922
    89
   relevance_convergence: real,
blanchet@36220
    90
   theory_relevant: bool option,
blanchet@36922
    91
   defs_relevant: bool,
blanchet@35969
    92
   isar_proof: bool,
blanchet@36924
    93
   isar_shrink_factor: int,
blanchet@35969
    94
   timeout: Time.time,
blanchet@35969
    95
   minimize_timeout: Time.time}
blanchet@35867
    96
blanchet@35867
    97
type problem =
blanchet@35969
    98
  {subgoal: int,
blanchet@35969
    99
   goal: Proof.context * (thm list * thm),
blanchet@35969
   100
   relevance_override: relevance_override,
blanchet@37500
   101
   axiom_clauses: cnf_thm list option,
blanchet@37500
   102
   filtered_clauses: cnf_thm list option}
blanchet@35867
   103
blanchet@36370
   104
datatype failure =
blanchet@37413
   105
  Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
blanchet@37413
   106
  MalformedInput | MalformedOutput | UnknownError
blanchet@36370
   107
blanchet@35867
   108
type prover_result =
blanchet@36370
   109
  {outcome: failure option,
blanchet@35969
   110
   message: string,
blanchet@36393
   111
   pool: name_pool option,
blanchet@35969
   112
   relevant_thm_names: string list,
blanchet@35969
   113
   atp_run_time_in_msecs: int,
blanchet@36369
   114
   output: string,
blanchet@35969
   115
   proof: string,
blanchet@35969
   116
   internal_thm_names: string Vector.vector,
blanchet@36400
   117
   conjecture_shape: int list list,
blanchet@37500
   118
   filtered_clauses: cnf_thm list}
blanchet@35867
   119
blanchet@36281
   120
type prover =
blanchet@36281
   121
  params -> minimize_command -> Time.time -> problem -> prover_result
blanchet@35867
   122
wenzelm@28582
   123
(* named provers *)
wenzelm@28484
   124
blanchet@36379
   125
structure Data = Theory_Data
wenzelm@28582
   126
(
blanchet@35867
   127
  type T = (prover * stamp) Symtab.table;
wenzelm@32938
   128
  val empty = Symtab.empty;
wenzelm@32938
   129
  val extend = I;
wenzelm@33522
   130
  fun merge data : T = Symtab.merge (eq_snd op =) data
blanchet@37580
   131
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   132
);
wenzelm@28484
   133
boehmes@32864
   134
fun add_prover (name, prover) thy =
blanchet@36379
   135
  Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
blanchet@37580
   136
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   137
wenzelm@32995
   138
fun get_prover thy name =
blanchet@37580
   139
  the (Symtab.lookup (Data.get thy) name) |> fst
blanchet@37580
   140
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
wenzelm@32995
   141
blanchet@36229
   142
fun available_atps thy =
blanchet@36229
   143
  priority ("Available ATPs: " ^
blanchet@36379
   144
            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
wenzelm@28571
   145
wenzelm@28586
   146
wenzelm@28595
   147
(* start prover thread *)
wenzelm@28484
   148
blanchet@37584
   149
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
blanchet@37584
   150
                        relevance_override minimize_command proof_state name =
blanchet@36379
   151
  let
blanchet@37584
   152
    val birth_time = Time.now ()
blanchet@37584
   153
    val death_time = Time.+ (birth_time, timeout)
blanchet@36379
   154
    val prover = get_prover (Proof.theory_of proof_state) name
blanchet@36379
   155
    val {context = ctxt, facts, goal} = Proof.goal proof_state;
blanchet@36379
   156
    val desc =
blanchet@36379
   157
      "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
blanchet@36392
   158
      Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
blanchet@37584
   159
  in
blanchet@37585
   160
    Async_Manager.launch das_Tool verbose birth_time death_time desc
blanchet@37584
   161
        (fn () =>
blanchet@37584
   162
            let
blanchet@37584
   163
              val problem =
blanchet@37584
   164
                {subgoal = i, goal = (ctxt, (facts, goal)),
blanchet@37584
   165
                 relevance_override = relevance_override, axiom_clauses = NONE,
blanchet@37584
   166
                 filtered_clauses = NONE}
blanchet@37584
   167
            in
blanchet@37584
   168
              prover params (minimize_command name) timeout problem |> #message
blanchet@37584
   169
              handle TRIVIAL () => metis_line full_types i n []
blanchet@37584
   170
                   | ERROR message => "Error: " ^ message ^ "\n"
blanchet@37584
   171
            end)
blanchet@37584
   172
  end
wenzelm@28582
   173
wenzelm@28582
   174
end;