1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:11 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:17 2014 +0200
     1.3 @@ -14,11 +14,9 @@
     1.4  
     1.5    type slice_spec = (int * string) * atp_format * string * string * bool
     1.6    type atp_config =
     1.7 -    {exec : unit -> string list * string list,
     1.8 -     arguments :
     1.9 -       Proof.context -> bool -> string -> Time.time -> string
    1.10 -       -> term_order * (unit -> (string * int) list)
    1.11 -          * (unit -> (string * real) list) -> string,
    1.12 +    {exec : bool -> string list * string list,
    1.13 +     arguments : Proof.context -> bool -> string -> Time.time -> string ->
    1.14 +       term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
    1.15       proof_delims : (string * string) list,
    1.16       known_failures : (atp_failure * string) list,
    1.17       prem_role : atp_formula_role,
    1.18 @@ -48,10 +46,9 @@
    1.19    val spass_H2NuVS0Red2 : string
    1.20    val spass_H2SOS : string
    1.21    val spass_extra_options : string Config.T
    1.22 -  val remote_atp :
    1.23 -    string -> string -> string list -> (string * string) list
    1.24 -    -> (atp_failure * string) list -> atp_formula_role
    1.25 -    -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
    1.26 +  val remote_atp : string -> string -> string list -> (string * string) list ->
    1.27 +    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
    1.28 +    string * (unit -> atp_config)
    1.29    val add_atp : string * (unit -> atp_config) -> theory -> theory
    1.30    val get_atp : theory -> string -> (unit -> atp_config)
    1.31    val supported_atps : theory -> string list
    1.32 @@ -76,11 +73,9 @@
    1.33  type slice_spec = (int * string) * atp_format * string * string * bool
    1.34  
    1.35  type atp_config =
    1.36 -  {exec : unit -> string list * string list,
    1.37 -   arguments :
    1.38 -     Proof.context -> bool -> string -> Time.time -> string
    1.39 -     -> term_order * (unit -> (string * int) list)
    1.40 -        * (unit -> (string * real) list) -> string,
    1.41 +  {exec : bool -> string list * string list,
    1.42 +   arguments : Proof.context -> bool -> string -> Time.time -> string ->
    1.43 +     term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
    1.44     proof_delims : (string * string) list,
    1.45     known_failures : (atp_failure * string) list,
    1.46     prem_role : atp_formula_role,
    1.47 @@ -213,7 +208,6 @@
    1.48  (* E *)
    1.49  
    1.50  fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
    1.51 -fun is_e_at_least_1_9 () = string_ord (getenv "E_VERSION", "1.9") <> LESS
    1.52  
    1.53  val e_smartN = "smart"
    1.54  val e_autoN = "auto"
    1.55 @@ -286,9 +280,10 @@
    1.56      end
    1.57  
    1.58  val e_config : atp_config =
    1.59 -  {exec = (fn () => (["E_HOME"],
    1.60 -     if is_e_at_least_1_9 () then ["eprover"] else ["eproof_ram", "eproof"])),
    1.61 -   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
    1.62 +  {exec = fn full_proofs => (["E_HOME"],
    1.63 +     if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
    1.64 +     else ["eprover"]),
    1.65 +   arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
    1.66       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    1.67         (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
    1.68         "--tstp-in --tstp-out --silent " ^
    1.69 @@ -296,8 +291,10 @@
    1.70         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
    1.71         "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
    1.72         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
    1.73 -       (if is_e_at_least_1_9 () then " --proof-object=3"
    1.74 -        else " --output-level=5 --pcl-shell-level=" ^ (if full_proof then "0" else "2")) ^
    1.75 +       (if full_proofs orelse not (is_e_at_least_1_8 ()) then
    1.76 +          " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
    1.77 +        else
    1.78 +          " --proof-object=1") ^
    1.79         " " ^ file_name,
    1.80     proof_delims =
    1.81       [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
    1.82 @@ -511,20 +508,20 @@
    1.83  
    1.84  val vampire_config : atp_config =
    1.85    {exec = K (["VAMPIRE_HOME"], ["vampire"]),
    1.86 -   arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
    1.87 +   arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name =>
    1.88         fn _ =>
    1.89         "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
    1.90         " --proof tptp --output_axiom_names on" ^
    1.91         (if is_vampire_at_least_1_8 () then
    1.92            (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
    1.93 -          (if full_proof then
    1.94 +          (if full_proofs then
    1.95               " --forced_options splitting=off:equality_proxy=off:general_splitting=off\
    1.96               \:inequality_splitting=0:naming=0"
    1.97             else
    1.98               "")
    1.99          else
   1.100            "") ^
   1.101 -       " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
   1.102 +       " --thanks \"Andrei et al.\" --input_file " ^ file_name
   1.103         |> sos = sosN ? prefix "--sos on ",
   1.104     proof_delims =
   1.105       [("=========== Refutation ==========",
   1.106 @@ -766,7 +763,7 @@
   1.107  
   1.108  fun is_atp_installed thy name =
   1.109    let val {exec, ...} = get_atp thy name () in
   1.110 -    exists (fn var => getenv var <> "") (fst (exec ()))
   1.111 +    exists (fn var => getenv var <> "") (fst (exec false))
   1.112    end
   1.113  
   1.114  fun refresh_systems_on_tptp () =

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jul 25 11:26:11 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jul 25 11:26:17 2014 +0200
     2.3 @@ -143,6 +143,7 @@
     2.4      val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
     2.5        best_max_new_mono_instances, ...} = get_atp thy name ()
     2.6  
     2.7 +    val full_proofs = isar_proofs |> the_default (mode = Minimize)
     2.8      val local_name = perhaps (try (unprefix remote_prefix)) name
     2.9      val waldmeister_new = (local_name = waldmeister_newN)
    2.10      val spass = (local_name = spassN orelse local_name = spass_pirateN)
    2.11 @@ -162,7 +163,7 @@
    2.12          Path.append (Path.explode dest_dir) problem_file_name
    2.13        else
    2.14          error ("No such directory: " ^ quote dest_dir ^ ".")
    2.15 -    val exec = exec ()
    2.16 +    val exec = exec full_proofs
    2.17      val command0 =
    2.18        (case find_first (fn var => getenv var <> "") (fst exec) of
    2.19          SOME var =>
    2.20 @@ -276,9 +277,8 @@
    2.21              fun ord_info () = atp_problem_term_order_info atp_problem
    2.22  
    2.23              val ord = effective_term_order ctxt name
    2.24 -            val full_proof = isar_proofs |> the_default (mode = Minimize)
    2.25              val args =
    2.26 -              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
    2.27 +              arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path)
    2.28                  (ord, ord_info, sel_weights)
    2.29              val command =
    2.30                "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"