src/HOL/Tools/ATP_Manager/atp_manager.ML
author blanchet
Tue Jul 27 17:04:09 2010 +0200 (2010-07-27 ago)
changeset 38015 b30c3c2e1030
parent 38002 31705eccee23
permissions -rw-r--r--
implemented "sublinear" minimization algorithm
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@35969
    11
  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
blanchet@36281
    12
  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
blanchet@35969
    13
  type params =
blanchet@35969
    14
    {debug: bool,
blanchet@35969
    15
     verbose: bool,
blanchet@36143
    16
     overlord: bool,
blanchet@35969
    17
     atps: string list,
blanchet@35969
    18
     full_types: bool,
blanchet@36235
    19
     explicit_apply: bool,
blanchet@35969
    20
     relevance_threshold: real,
blanchet@36922
    21
     relevance_convergence: real,
blanchet@36220
    22
     theory_relevant: bool option,
blanchet@36922
    23
     defs_relevant: bool,
blanchet@35969
    24
     isar_proof: bool,
blanchet@36924
    25
     isar_shrink_factor: int,
blanchet@35969
    26
     timeout: Time.time,
blanchet@35969
    27
     minimize_timeout: Time.time}
blanchet@35867
    28
  type problem =
blanchet@35969
    29
    {subgoal: int,
blanchet@35969
    30
     goal: Proof.context * (thm list * thm),
blanchet@35969
    31
     relevance_override: relevance_override,
blanchet@38002
    32
     axiom_clauses: (string * thm) list option,
blanchet@38002
    33
     filtered_clauses: (string * thm) list option}
blanchet@36370
    34
  datatype failure =
blanchet@37627
    35
    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
blanchet@37627
    36
    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
blanchet@35867
    37
  type prover_result =
blanchet@36370
    38
    {outcome: failure option,
blanchet@35969
    39
     message: string,
blanchet@37926
    40
     pool: string Symtab.table,
blanchet@38015
    41
     used_thm_names: string list,
blanchet@35969
    42
     atp_run_time_in_msecs: int,
blanchet@36369
    43
     output: string,
blanchet@35969
    44
     proof: string,
blanchet@35969
    45
     internal_thm_names: string Vector.vector,
blanchet@37996
    46
     conjecture_shape: int list,
blanchet@38002
    47
     filtered_clauses: (string * thm) list}
blanchet@36281
    48
  type prover =
blanchet@36281
    49
    params -> minimize_command -> Time.time -> problem -> prover_result
blanchet@35867
    50
blanchet@35969
    51
  val kill_atps: unit -> unit
blanchet@35969
    52
  val running_atps: unit -> unit
wenzelm@29112
    53
  val messages: int option -> unit
blanchet@35867
    54
  val add_prover: string * prover -> theory -> theory
blanchet@36379
    55
  val get_prover: theory -> string -> prover
blanchet@35969
    56
  val available_atps: theory -> unit
blanchet@37584
    57
  val start_prover_thread :
blanchet@37584
    58
    params -> int -> int -> relevance_override -> (string -> minimize_command)
blanchet@37584
    59
    -> Proof.state -> string -> unit
wenzelm@28477
    60
end;
wenzelm@28477
    61
blanchet@35865
    62
structure ATP_Manager : ATP_MANAGER =
wenzelm@28477
    63
struct
wenzelm@28477
    64
blanchet@37578
    65
open Metis_Clauses
blanchet@36063
    66
open Sledgehammer_Fact_Filter
blanchet@36063
    67
open Sledgehammer_Proof_Reconstruct
blanchet@37583
    68
blanchet@37583
    69
(** The Sledgehammer **)
blanchet@37583
    70
blanchet@37585
    71
val das_Tool = "Sledgehammer"
blanchet@37585
    72
blanchet@37585
    73
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
blanchet@37585
    74
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
blanchet@37585
    75
val messages = Async_Manager.thread_messages das_Tool "ATP"
blanchet@35969
    76
blanchet@36281
    77
(** problems, results, provers, etc. **)
blanchet@35969
    78
blanchet@35969
    79
type params =
blanchet@35969
    80
  {debug: bool,
blanchet@35969
    81
   verbose: bool,
blanchet@36143
    82
   overlord: bool,
blanchet@35969
    83
   atps: string list,
blanchet@35969
    84
   full_types: bool,
blanchet@36235
    85
   explicit_apply: bool,
blanchet@35969
    86
   relevance_threshold: real,
blanchet@36922
    87
   relevance_convergence: real,
blanchet@36220
    88
   theory_relevant: bool option,
blanchet@36922
    89
   defs_relevant: bool,
blanchet@35969
    90
   isar_proof: bool,
blanchet@36924
    91
   isar_shrink_factor: int,
blanchet@35969
    92
   timeout: Time.time,
blanchet@35969
    93
   minimize_timeout: Time.time}
blanchet@35867
    94
blanchet@35867
    95
type problem =
blanchet@35969
    96
  {subgoal: int,
blanchet@35969
    97
   goal: Proof.context * (thm list * thm),
blanchet@35969
    98
   relevance_override: relevance_override,
blanchet@38002
    99
   axiom_clauses: (string * thm) list option,
blanchet@38002
   100
   filtered_clauses: (string * thm) list option}
blanchet@35867
   101
blanchet@36370
   102
datatype failure =
blanchet@37627
   103
  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
blanchet@37627
   104
  OldSpass | MalformedInput | MalformedOutput | UnknownError
blanchet@36370
   105
blanchet@35867
   106
type prover_result =
blanchet@36370
   107
  {outcome: failure option,
blanchet@35969
   108
   message: string,
blanchet@37926
   109
   pool: string Symtab.table,
blanchet@38015
   110
   used_thm_names: string list,
blanchet@35969
   111
   atp_run_time_in_msecs: int,
blanchet@36369
   112
   output: string,
blanchet@35969
   113
   proof: string,
blanchet@35969
   114
   internal_thm_names: string Vector.vector,
blanchet@37996
   115
   conjecture_shape: int list,
blanchet@38002
   116
   filtered_clauses: (string * thm) list}
blanchet@35867
   117
blanchet@36281
   118
type prover =
blanchet@36281
   119
  params -> minimize_command -> Time.time -> problem -> prover_result
blanchet@35867
   120
wenzelm@28582
   121
(* named provers *)
wenzelm@28484
   122
blanchet@36379
   123
structure Data = Theory_Data
wenzelm@28582
   124
(
blanchet@35867
   125
  type T = (prover * stamp) Symtab.table;
wenzelm@32938
   126
  val empty = Symtab.empty;
wenzelm@32938
   127
  val extend = I;
wenzelm@33522
   128
  fun merge data : T = Symtab.merge (eq_snd op =) data
blanchet@37580
   129
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   130
);
wenzelm@28484
   131
boehmes@32864
   132
fun add_prover (name, prover) thy =
blanchet@36379
   133
  Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
blanchet@37580
   134
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
wenzelm@28582
   135
wenzelm@32995
   136
fun get_prover thy name =
blanchet@37580
   137
  the (Symtab.lookup (Data.get thy) name) |> fst
blanchet@37580
   138
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
wenzelm@32995
   139
blanchet@36229
   140
fun available_atps thy =
blanchet@36229
   141
  priority ("Available ATPs: " ^
blanchet@36379
   142
            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
wenzelm@28571
   143
wenzelm@28586
   144
wenzelm@28595
   145
(* start prover thread *)
wenzelm@28484
   146
blanchet@37584
   147
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
blanchet@37584
   148
                        relevance_override minimize_command proof_state name =
blanchet@36379
   149
  let
blanchet@37584
   150
    val birth_time = Time.now ()
blanchet@37584
   151
    val death_time = Time.+ (birth_time, timeout)
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@37584
   157
  in
blanchet@37585
   158
    Async_Manager.launch das_Tool verbose birth_time death_time desc
blanchet@37584
   159
        (fn () =>
blanchet@37584
   160
            let
blanchet@37584
   161
              val problem =
blanchet@37584
   162
                {subgoal = i, goal = (ctxt, (facts, goal)),
blanchet@37584
   163
                 relevance_override = relevance_override, axiom_clauses = NONE,
blanchet@37584
   164
                 filtered_clauses = NONE}
blanchet@37584
   165
            in
blanchet@37584
   166
              prover params (minimize_command name) timeout problem |> #message
blanchet@37994
   167
              handle ERROR message => "Error: " ^ message ^ "\n"
blanchet@37584
   168
            end)
blanchet@37584
   169
  end
wenzelm@28582
   170
wenzelm@28582
   171
end;