# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 7a43449ffd861b9a402855105c6a7e2c01971a63
# Parent  6e0cb8044734cd215deb2d0d1c7f28371c474052
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout

diff -r 6e0cb8044734 -r 7a43449ffd86 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 17:00:38 2011 +0200
@@ -117,18 +117,11 @@
     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
 )
 
-fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
+fun to_secs time = (Time.toMilliseconds time + 999) div 1000
 
 
 (* E *)
 
-(* Give E an extra second to reconstruct the proof. Older versions even get two
-   seconds, because the "eproof" script wrongly subtracted an entire second to
-   account for the overhead of the script itself, which is in fact much
-   lower. *)
-fun e_bonus () =
-  if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
-
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
@@ -210,8 +203,7 @@
    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 (e_bonus ()) timeout),
+     " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
@@ -251,7 +243,7 @@
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
+      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
      |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
@@ -286,7 +278,7 @@
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
-     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+     "--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)
         ? prefix "--sos on ",
@@ -325,7 +317,7 @@
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
+     "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
    proof_delims = [],
    known_failures =
      [(Unprovable, "\nsat"),
@@ -382,7 +374,7 @@
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn timeout => fn _ =>
-     "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
+     "-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,
    known_failures = known_failures @ known_perl_failures @