# HG changeset patch
# User blanchet
# Date 1271262231 -7200
# Node ID f5e15e9aae10df54e81445636c8b087125a7e1cd
# Parent  c31602d268bef25ccc4fa82bba773a2aab61af59
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

diff -r c31602d268be -r f5e15e9aae10 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 17:10:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 18:23:51 2010 +0200
@@ -22,6 +22,7 @@
 structure ATP_Minimal : ATP_MINIMAL =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_Proof_Reconstruct
 open ATP_Manager
@@ -114,8 +115,9 @@
 fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
         timeout subgoal state filtered name_thms_pairs =
   let
-    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
-                      " theorems... ")
+    val num_theorems = length name_thms_pairs
+    val _ = priority ("Testing " ^ string_of_int num_theorems ^
+                      " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
@@ -161,12 +163,17 @@
             ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
         in (SOME min_thms, metis_line i n min_names) end
     | (Timeout, _) =>
-        (NONE, "Timeout: You may need to increase the time limit of " ^
-          string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
+        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
+               \option (e.g., \"timeout = " ^
+               string_of_int (10 + msecs div 1000) ^ " s\").")
     | (Error, msg) =>
         (NONE, "Error in prover: " ^ msg)
     | (Failure, _) =>
-        (NONE, "Failure: No proof with the theorems supplied"))
+        (* Failure sometimes mean timeout, unfortunately. *)
+        (NONE, "Failure: No proof was found with the current time limit. You \
+               \can increase the time limit using the \"timeout\" \
+               \option (e.g., \"timeout = " ^
+               string_of_int (10 + msecs div 1000) ^ " s\")."))
     handle Sledgehammer_HOL_Clause.TRIVIAL =>
         (SOME [], metis_line i n [])
       | ERROR msg => (NONE, "Error: " ^ msg)
diff -r c31602d268be -r f5e15e9aae10 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 17:10:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 18:23:51 2010 +0200
@@ -179,6 +179,8 @@
 
 (** common provers **)
 
+fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
+
 (* Vampire *)
 
 (* NB: Vampire does not work without explicit time limit. *)
@@ -186,7 +188,7 @@
 val vampire_config : prover_config =
   {command = Path.explode "$VAMPIRE_HOME/vampire",
    arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
-                              string_of_int (Time.toSeconds timeout)),
+                              string_of_int (generous_to_secs timeout)),
    failure_strs =
      ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
    max_new_clauses = 60,
@@ -201,7 +203,7 @@
   {command = Path.explode "$E_HOME/eproof",
    arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
                               \-tAutoDev --silent --cpu-limit=" ^
-                              string_of_int (Time.toSeconds timeout)),
+                              string_of_int (generous_to_secs timeout)),
    failure_strs =
        ["SZS status: Satisfiable", "SZS status Satisfiable",
         "SZS status: ResourceOut", "SZS status ResourceOut",
@@ -233,7 +235,7 @@
  {command = Path.explode "$SPASS_HOME/SPASS",
   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
     " -FullRed=0 -DocProof -TimeLimit=" ^
-    string_of_int (Time.toSeconds timeout)),
+    string_of_int (generous_to_secs timeout)),
   failure_strs =
     ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
      "SPASS beiseite: Maximal number of loops exceeded."],
@@ -276,7 +278,7 @@
          : prover_config) : prover_config =
   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    arguments = (fn timeout =>
-     args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
+     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
      the_system prover_prefix),
    failure_strs = remote_failure_strs @ failure_strs,
    max_new_clauses = max_new_clauses,
diff -r c31602d268be -r f5e15e9aae10 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 17:10:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 18:23:51 2010 +0200
@@ -100,7 +100,10 @@
   |> fold (AList.default (op =))
           [("atps", [!atps]),
            ("full_types", [if !full_types then "true" else "false"]),
-           ("timeout", [string_of_int (!timeout) ^ " s"])]
+           ("timeout", let val timeout = !timeout in
+                         [if timeout <= 0 then "none"
+                          else string_of_int timeout ^ " s"]
+                       end)]
 
 val infinity_time_in_secs = 60 * 60 * 24 * 365
 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
@@ -181,7 +184,7 @@
       get_params thy
           [("atps", [atp]),
            ("minimize_timeout",
-            [string_of_int (Time.toSeconds timeout) ^ " s"])]
+            [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]
     val prover =
       (case get_prover thy atp of
         SOME prover => prover
diff -r c31602d268be -r f5e15e9aae10 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 17:10:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 18:23:51 2010 +0200
@@ -6,6 +6,7 @@
 
 signature SLEDGEHAMMER_UTIL =
 sig
+  val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
@@ -17,12 +18,7 @@
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
 struct
 
-(* This hash function is recommended in Compilers: Principles, Techniques, and
-   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
-   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
-fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
-fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
-fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
+fun plural_s n = if n = 1 then "" else "s"
 
 fun serial_commas _ [] = ["??"]
   | serial_commas _ [s] = [s]
@@ -60,4 +56,11 @@
         SOME (Time.fromMilliseconds msecs)
     end
 
+(* This hash function is recommended in Compilers: Principles, Techniques, and
+   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
+   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
+fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
+fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
+fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
+
 end;