--- 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 @