Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
author wenzelm
Mon, 05 Aug 2013 15:03:52 +0200
changeset 52861 e93d73b51fd0
parent 52590 02713cd2c2cd
child 54495 237d5be57277
permissions -rw-r--r--
commands with overlay remain visible, to avoid loosing printed output;

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Steffen Juilf Smolka, TU Muenchen

Reconstructors.
*)

signature SLEDGEHAMMER_RECONSTRUCTOR =
sig

  type stature = ATP_Problem_Generate.stature

  datatype reconstructor =
    Metis of string * string |
    SMT

  datatype play =
    Played of reconstructor * Time.time |
    Trust_Playable of reconstructor * Time.time option |
    Failed_to_Play of reconstructor

  type minimize_command = string list -> string

  type one_line_params =
    play * string * (string * stature) list * minimize_command * int * int

  val smtN : string

end

structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
struct

open ATP_Problem_Generate

datatype reconstructor =
  Metis of string * string |
  SMT

datatype play =
  Played of reconstructor * Time.time |
  Trust_Playable of reconstructor * Time.time option |
  Failed_to_Play of reconstructor

type minimize_command = string list -> string

type one_line_params =
  play * string * (string * stature) list * minimize_command * int * int

val smtN = "smt"

end
isabelle