pass timeout to prover;
especially to remote-script

--- a/src/HOL/ATP_Linkup.thy	Tue Jan 20 18:12:06 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy	Tue Jan 20 20:58:08 2009 +0100
@@ -113,11 +113,11 @@
 
 text {* remote provers via SystemOnTPTP *}
 setup {* AtpManager.add_prover "remote_vampire"
-  (AtpWrapper.remote_prover "-s Vampire---9.0 -t 100") *}
+  (AtpWrapper.remote_prover "-s Vampire---9.0") *}
 setup {* AtpManager.add_prover "remote_spass"
-  (AtpWrapper.remote_prover "-s SPASS---3.01 -t 100") *}
+  (AtpWrapper.remote_prover "-s SPASS---3.01") *}
 setup {* AtpManager.add_prover "remote_e"
-  (AtpWrapper.remote_prover "-s EP---1.0 -t 100") *}
+  (AtpWrapper.remote_prover "-s EP---1.0") *}
   
 
 

--- a/src/HOL/Tools/atp_manager.ML	Tue Jan 20 18:12:06 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML	Tue Jan 20 20:58:08 2009 +0100
@@ -19,7 +19,7 @@
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
-  type prover = int -> Proof.state -> bool * string
+  type prover = int -> int -> Proof.state -> bool * string
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val sledgehammer: string list -> Proof.state -> unit
@@ -264,7 +264,7 @@
 
 (* named provers *)
 
-type prover = int -> Proof.state -> bool * string;
+type prover = int -> int -> Proof.state -> bool * string;
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
@@ -300,7 +300,7 @@
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
-            val result = prover i proof_state
+            val result = prover (get_timeout ()) i proof_state
               handle ResHolClause.TOO_TRIVIAL
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
               | ERROR msg

--- a/src/HOL/Tools/atp_wrapper.ML	Tue Jan 20 18:12:06 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jan 20 20:58:08 2009 +0100
@@ -47,7 +47,7 @@
 
 (* basic template *)
 
-fun external_prover write_problem_files (cmd, args) find_failure produce_answer subgoalno state =
+fun external_prover write_problem_files (cmd, args) find_failure produce_answer timeout subgoalno state =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -114,15 +114,19 @@
 
 (*NB: Vampire does not work without explicit timelimit*)
 
-fun vampire_opts max_new theory_const = tptp_prover_opts
+fun vampire_opts max_new theory_const timeout = tptp_prover_opts
   max_new theory_const
-  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+  (Path.explode "$VAMPIRE_HOME/vampire",
+               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+  timeout;
 
 val vampire = vampire_opts 60 false;
 
-fun vampire_opts_full max_new theory_const = full_prover_opts
+fun vampire_opts_full max_new theory_const timeout = full_prover_opts
   max_new theory_const
-  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+  (Path.explode "$VAMPIRE_HOME/vampire",
+               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+  timeout;
 
 val vampire_full = vampire_opts 60 false;
 
@@ -155,9 +159,10 @@
 
 (* remote prover invocation via SystemOnTPTP *)
 
-fun remote_prover_opts max_new theory_const args =
+fun remote_prover_opts max_new theory_const args timeout =
   tptp_prover_opts max_new theory_const
-  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args);
+  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
+  timeout;
 
 val remote_prover = remote_prover_opts 60 false;