1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jun 10 12:01:15 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4      {exec : string * string,
     1.5       required_execs : (string * string) list,
     1.6       arguments :
     1.7 -       Proof.context -> int -> Time.time -> (unit -> (string * real) list)
     1.8 -       -> string,
     1.9 +       Proof.context -> bool -> int -> Time.time
    1.10 +       -> (unit -> (string * real) list) -> string,
    1.11       proof_delims : (string * string) list,
    1.12       known_failures : (failure * string) list,
    1.13       conj_sym_kind : formula_kind,
    1.14 @@ -68,7 +68,7 @@
    1.15    {exec : string * string,
    1.16     required_execs : (string * string) list,
    1.17     arguments :
    1.18 -     Proof.context -> int -> Time.time -> (unit -> (string * real) list)
    1.19 +     Proof.context -> bool -> int -> Time.time -> (unit -> (string * real) list)
    1.20       -> string,
    1.21     proof_delims : (string * string) list,
    1.22     known_failures : (failure * string) list,
    1.23 @@ -200,10 +200,12 @@
    1.24  val e_config : atp_config =
    1.25    {exec = ("E_HOME", "eproof"),
    1.26     required_execs = [],
    1.27 -   arguments = fn ctxt => fn slice => fn timeout => fn weights =>
    1.28 -     "--tstp-in --tstp-out -l5 " ^
    1.29 -     e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
    1.30 -     " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    1.31 +   arguments =
    1.32 +     fn ctxt => fn full_proof => fn slice => fn timeout => fn weights =>
    1.33 +        "--tstp-in --tstp-out -l5 " ^
    1.34 +        e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
    1.35 +        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
    1.36 +        (if full_proof orelse is_old_e_version () then "" else " --trim"),
    1.37     proof_delims = tstp_proof_delims,
    1.38     known_failures =
    1.39       [(Unprovable, "SZS status: CounterSatisfiable"),
    1.40 @@ -241,7 +243,7 @@
    1.41  val spass_config : atp_config =
    1.42    {exec = ("ISABELLE_ATP", "scripts/spass"),
    1.43     required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    1.44 -   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
    1.45 +   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
    1.46       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    1.47        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
    1.48       |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
    1.49 @@ -277,7 +279,7 @@
    1.50  val vampire_config : atp_config =
    1.51    {exec = ("VAMPIRE_HOME", "vampire"),
    1.52     required_execs = [],
    1.53 -   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
    1.54 +   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
    1.55       "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
    1.56       " --thanks \"Andrei and Krystof\" --input_file"
    1.57       |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
    1.58 @@ -316,7 +318,7 @@
    1.59  val z3_atp_config : atp_config =
    1.60    {exec = ("Z3_HOME", "z3"),
    1.61     required_execs = [],
    1.62 -   arguments = fn _ => fn _ => fn timeout => fn _ =>
    1.63 +   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
    1.64       "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
    1.65     proof_delims = [],
    1.66     known_failures =
    1.67 @@ -373,7 +375,7 @@
    1.68                    conj_sym_kind prem_kind formats best_slice : atp_config =
    1.69    {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    1.70     required_execs = [],
    1.71 -   arguments = fn _ => fn _ => fn timeout => fn _ =>
    1.72 +   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
    1.73       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
    1.74       ^ " -s " ^ the_system system_name system_versions,
    1.75     proof_delims = union (op =) tstp_proof_delims proof_delims,