be more generous towards SPASS's -SOS mode

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Aug 22 16:56:05 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Aug 22 22:47:03 2010 +0200
@@ -16,6 +16,7 @@
     {exec: string * string,
      required_execs: (string * string) list,
      arguments: bool -> Time.time -> string,
+     has_incomplete_mode: bool,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
      default_max_relevant_per_iter: int,
@@ -48,6 +49,7 @@
   {exec: string * string,
    required_execs: (string * string) list,
    arguments: bool -> Time.time -> string,
+   has_incomplete_mode: bool,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
    default_max_relevant_per_iter: int,
@@ -136,6 +138,7 @@
    arguments = fn _ => fn timeout =>
      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
      string_of_int (to_generous_secs timeout),
+   has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
@@ -162,9 +165,9 @@
    (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^
-      string_of_int ((to_generous_secs timeout + 1) div 2))
+      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
      |> not complete ? prefix "-SOS=1 ",
+   has_incomplete_mode = true,
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
@@ -190,6 +193,7 @@
    arguments = fn _ => fn timeout =>
      "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
      " --thanks Andrei --input_file",
+   has_incomplete_mode = false,
    proof_delims =
      [("=========== Refutation ==========",
        "======= End of refutation ======="),
@@ -242,6 +246,7 @@
    arguments = fn _ => fn timeout =>
      " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
      the_system system_prefix,
+   has_incomplete_mode = false,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =
      known_failures @ known_perl_failures @

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 22 16:56:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 22 22:47:03 2010 +0200
@@ -207,8 +207,8 @@
 (* generic TPTP-based provers *)
 
 fun prover_fun atp_name
-        {exec, required_execs, arguments, proof_delims, known_failures,
-         default_max_relevant_per_iter, default_theory_relevant,
+        {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
+         known_failures, default_max_relevant_per_iter, default_theory_relevant,
          explicit_forall, use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           relevance_threshold, relevance_convergence,
@@ -260,7 +260,7 @@
 
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     (* write out problem file and call prover *)
-    fun command_line complete probfile =
+    fun command_line complete timeout probfile =
       let
         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
                    " " ^ File.shell_path probfile
@@ -288,9 +288,9 @@
       | [] =>
         if File.exists command then
           let
-            fun do_run complete =
+            fun do_run complete timeout =
               let
-                val command = command_line complete probfile
+                val command = command_line complete timeout probfile
                 val ((output, msecs), res_code) =
                   bash_output command
                   |>> (if overlord then
@@ -316,13 +316,20 @@
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
               |> map single
             val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
+            val timer = Timer.startRealTimer ()
             val result =
-              do_run false
-              |> (fn (_, msecs0, _, SOME _) =>
-                     do_run true
-                     |> (fn (output, msecs, proof, outcome) =>
-                            (output, msecs0 + msecs, proof, outcome))
-                   | result => result)
+              do_run false (if has_incomplete_mode then
+                              Time.fromMilliseconds
+                                         (2 * Time.toMilliseconds timeout div 3)
+                            else
+                              timeout)
+              |> has_incomplete_mode
+                 ? (fn (_, msecs0, _, SOME _) =>
+                       do_run true
+                              (Time.- (timeout, Timer.checkRealTimer timer))
+                       |> (fn (output, msecs, proof, outcome) =>
+                              (output, msecs0 + msecs, proof, outcome))
+                     | result => result)
           in ((pool, conjecture_shape, axiom_names), result) end
         else
           error ("Bad executable: " ^ Path.implode command ^ ".")