# HG changeset patch
# User blanchet
# Date 1307700075 -7200
# Node ID 396aaa15dd8bbd9d779e6723134ab71858fbb455
# Parent  6c008d3efb0a3d5b3a28c2ed52271b8f49ab2150
pass --trim option to "eproof" script to speed up proof reconstruction

diff -r 6c008d3efb0a -r 396aaa15dd8b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jun 10 12:01:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jun 10 12:01:15 2011 +0200
@@ -15,8 +15,8 @@
     {exec : string * string,
      required_execs : (string * string) list,
      arguments :
-       Proof.context -> int -> Time.time -> (unit -> (string * real) list)
-       -> string,
+       Proof.context -> bool -> int -> Time.time
+       -> (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
@@ -68,7 +68,7 @@
   {exec : string * string,
    required_execs : (string * string) list,
    arguments :
-     Proof.context -> int -> Time.time -> (unit -> (string * real) list)
+     Proof.context -> bool -> int -> Time.time -> (unit -> (string * real) list)
      -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
@@ -200,10 +200,12 @@
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
-   arguments = fn ctxt => fn slice => fn timeout => fn weights =>
-     "--tstp-in --tstp-out -l5 " ^
-     e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
-     " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
+   arguments =
+     fn ctxt => fn full_proof => fn slice => fn timeout => fn weights =>
+        "--tstp-in --tstp-out -l5 " ^
+        e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
+        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
+        (if full_proof orelse is_old_e_version () then "" else " --trim"),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
@@ -241,7 +243,7 @@
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
      |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
@@ -277,7 +279,7 @@
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
      "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
      |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
@@ -316,7 +318,7 @@
 val z3_atp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
-   arguments = fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
      "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
    proof_delims = [],
    known_failures =
@@ -373,7 +375,7 @@
                   conj_sym_kind prem_kind formats best_slice : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
-   arguments = fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
diff -r 6c008d3efb0a -r 396aaa15dd8b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 12:01:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 12:01:15 2011 +0200
@@ -654,7 +654,7 @@
                 fun weights () = atp_problem_weights atp_problem
                 val core =
                   File.shell_path command ^ " " ^
-                  arguments ctxt slice slice_timeout weights ^ " " ^
+                  arguments ctxt isar_proof slice slice_timeout weights ^ " " ^
                   File.shell_path prob_file
                 val command =
                   (if measure_run_time then