src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54495 237d5be57277
child 54772 f5fd4a34b0e8
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
smolkas@52590
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
smolkas@52555
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@52555
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52555
     4
smolkas@52555
     5
Reconstructors.
smolkas@52555
     6
*)
smolkas@52555
     7
smolkas@52555
     8
signature SLEDGEHAMMER_RECONSTRUCTOR =
smolkas@52555
     9
sig
smolkas@52555
    10
  type stature = ATP_Problem_Generate.stature
smolkas@52555
    11
smolkas@52555
    12
  datatype reconstructor =
smolkas@52555
    13
    Metis of string * string |
smolkas@52555
    14
    SMT
smolkas@52555
    15
smolkas@52555
    16
  datatype play =
smolkas@52555
    17
    Played of reconstructor * Time.time |
smolkas@52555
    18
    Trust_Playable of reconstructor * Time.time option |
smolkas@52555
    19
    Failed_to_Play of reconstructor
smolkas@52555
    20
smolkas@52555
    21
  type minimize_command = string list -> string
smolkas@52555
    22
smolkas@52555
    23
  type one_line_params =
smolkas@52555
    24
    play * string * (string * stature) list * minimize_command * int * int
smolkas@52555
    25
smolkas@52555
    26
  val smtN : string
blanchet@54495
    27
end;
smolkas@52555
    28
smolkas@52555
    29
structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
smolkas@52555
    30
struct
smolkas@52555
    31
smolkas@52555
    32
open ATP_Problem_Generate
smolkas@52555
    33
smolkas@52555
    34
datatype reconstructor =
smolkas@52555
    35
  Metis of string * string |
smolkas@52555
    36
  SMT
smolkas@52555
    37
smolkas@52555
    38
datatype play =
smolkas@52555
    39
  Played of reconstructor * Time.time |
smolkas@52555
    40
  Trust_Playable of reconstructor * Time.time option |
smolkas@52555
    41
  Failed_to_Play of reconstructor
smolkas@52555
    42
smolkas@52555
    43
type minimize_command = string list -> string
smolkas@52555
    44
smolkas@52555
    45
type one_line_params =
smolkas@52555
    46
  play * string * (string * stature) list * minimize_command * int * int
smolkas@52555
    47
smolkas@52555
    48
val smtN = "smt"
smolkas@52555
    49
blanchet@54495
    50
end;