src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML

avoid hardwired /bin/bash (like canonical Isabelle shell scripts);

(*  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_outcome =
    Played of Time.time |
    Play_Timed_Out of Time.time |
    Play_Failed |
    Not_Played

  val string_of_play_outcome: play_outcome -> string

  type minimize_command = string list -> string
  type one_line_params =
    (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int

  val smtN : string
end;

structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
struct

open ATP_Util
open ATP_Problem_Generate

datatype reconstructor =
  Metis of string * string |
  SMT

datatype play_outcome =
  Played of Time.time |
  Play_Timed_Out of Time.time |
  Play_Failed |
  Not_Played

fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
  | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
  | string_of_play_outcome Play_Failed = "failed"
  | string_of_play_outcome _ = "unknown"

type minimize_command = string list -> string
type one_line_params =
  (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int

val smtN = "smt"

end;