make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
authorblanchet
Wed Apr 14 18:23:51 2010 +0200 (2010-04-14 ago)
changeset 36142f5e15e9aae10
parent 36141 c31602d268be
child 36143 6490319b1703
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 17:10:16 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 18:23:51 2010 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  structure ATP_Minimal : ATP_MINIMAL =
     1.5  struct
     1.6  
     1.7 +open Sledgehammer_Util
     1.8  open Sledgehammer_Fact_Preprocessor
     1.9  open Sledgehammer_Proof_Reconstruct
    1.10  open ATP_Manager
    1.11 @@ -114,8 +115,9 @@
    1.12  fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
    1.13          timeout subgoal state filtered name_thms_pairs =
    1.14    let
    1.15 -    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
    1.16 -                      " theorems... ")
    1.17 +    val num_theorems = length name_thms_pairs
    1.18 +    val _ = priority ("Testing " ^ string_of_int num_theorems ^
    1.19 +                      " theorem" ^ plural_s num_theorems ^ "...")
    1.20      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    1.21      val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    1.22      val {context = ctxt, facts, goal} = Proof.goal state
    1.23 @@ -161,12 +163,17 @@
    1.24              ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
    1.25          in (SOME min_thms, metis_line i n min_names) end
    1.26      | (Timeout, _) =>
    1.27 -        (NONE, "Timeout: You may need to increase the time limit of " ^
    1.28 -          string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
    1.29 +        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
    1.30 +               \option (e.g., \"timeout = " ^
    1.31 +               string_of_int (10 + msecs div 1000) ^ " s\").")
    1.32      | (Error, msg) =>
    1.33          (NONE, "Error in prover: " ^ msg)
    1.34      | (Failure, _) =>
    1.35 -        (NONE, "Failure: No proof with the theorems supplied"))
    1.36 +        (* Failure sometimes mean timeout, unfortunately. *)
    1.37 +        (NONE, "Failure: No proof was found with the current time limit. You \
    1.38 +               \can increase the time limit using the \"timeout\" \
    1.39 +               \option (e.g., \"timeout = " ^
    1.40 +               string_of_int (10 + msecs div 1000) ^ " s\")."))
    1.41      handle Sledgehammer_HOL_Clause.TRIVIAL =>
    1.42          (SOME [], metis_line i n [])
    1.43        | ERROR msg => (NONE, "Error: " ^ msg)
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 17:10:16 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 18:23:51 2010 +0200
     2.3 @@ -179,6 +179,8 @@
     2.4  
     2.5  (** common provers **)
     2.6  
     2.7 +fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
     2.8 +
     2.9  (* Vampire *)
    2.10  
    2.11  (* NB: Vampire does not work without explicit time limit. *)
    2.12 @@ -186,7 +188,7 @@
    2.13  val vampire_config : prover_config =
    2.14    {command = Path.explode "$VAMPIRE_HOME/vampire",
    2.15     arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
    2.16 -                              string_of_int (Time.toSeconds timeout)),
    2.17 +                              string_of_int (generous_to_secs timeout)),
    2.18     failure_strs =
    2.19       ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
    2.20     max_new_clauses = 60,
    2.21 @@ -201,7 +203,7 @@
    2.22    {command = Path.explode "$E_HOME/eproof",
    2.23     arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
    2.24                                \-tAutoDev --silent --cpu-limit=" ^
    2.25 -                              string_of_int (Time.toSeconds timeout)),
    2.26 +                              string_of_int (generous_to_secs timeout)),
    2.27     failure_strs =
    2.28         ["SZS status: Satisfiable", "SZS status Satisfiable",
    2.29          "SZS status: ResourceOut", "SZS status ResourceOut",
    2.30 @@ -233,7 +235,7 @@
    2.31   {command = Path.explode "$SPASS_HOME/SPASS",
    2.32    arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
    2.33      " -FullRed=0 -DocProof -TimeLimit=" ^
    2.34 -    string_of_int (Time.toSeconds timeout)),
    2.35 +    string_of_int (generous_to_secs timeout)),
    2.36    failure_strs =
    2.37      ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
    2.38       "SPASS beiseite: Maximal number of loops exceeded."],
    2.39 @@ -276,7 +278,7 @@
    2.40           : prover_config) : prover_config =
    2.41    {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    2.42     arguments = (fn timeout =>
    2.43 -     args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
    2.44 +     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
    2.45       the_system prover_prefix),
    2.46     failure_strs = remote_failure_strs @ failure_strs,
    2.47     max_new_clauses = max_new_clauses,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 17:10:16 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 18:23:51 2010 +0200
     3.3 @@ -100,7 +100,10 @@
     3.4    |> fold (AList.default (op =))
     3.5            [("atps", [!atps]),
     3.6             ("full_types", [if !full_types then "true" else "false"]),
     3.7 -           ("timeout", [string_of_int (!timeout) ^ " s"])]
     3.8 +           ("timeout", let val timeout = !timeout in
     3.9 +                         [if timeout <= 0 then "none"
    3.10 +                          else string_of_int timeout ^ " s"]
    3.11 +                       end)]
    3.12  
    3.13  val infinity_time_in_secs = 60 * 60 * 24 * 365
    3.14  val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
    3.15 @@ -181,7 +184,7 @@
    3.16        get_params thy
    3.17            [("atps", [atp]),
    3.18             ("minimize_timeout",
    3.19 -            [string_of_int (Time.toSeconds timeout) ^ " s"])]
    3.20 +            [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]
    3.21      val prover =
    3.22        (case get_prover thy atp of
    3.23          SOME prover => prover
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 17:10:16 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 18:23:51 2010 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature SLEDGEHAMMER_UTIL =
     4.6  sig
     4.7 +  val plural_s : int -> string
     4.8    val serial_commas : string -> string list -> string list
     4.9    val parse_bool_option : bool -> string -> string -> bool option
    4.10    val parse_time_option : string -> string -> Time.time option
    4.11 @@ -17,12 +18,7 @@
    4.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    4.13  struct
    4.14  
    4.15 -(* This hash function is recommended in Compilers: Principles, Techniques, and
    4.16 -   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    4.17 -   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    4.18 -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    4.19 -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    4.20 -fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    4.21 +fun plural_s n = if n = 1 then "" else "s"
    4.22  
    4.23  fun serial_commas _ [] = ["??"]
    4.24    | serial_commas _ [s] = [s]
    4.25 @@ -60,4 +56,11 @@
    4.26          SOME (Time.fromMilliseconds msecs)
    4.27      end
    4.28  
    4.29 +(* This hash function is recommended in Compilers: Principles, Techniques, and
    4.30 +   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    4.31 +   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    4.32 +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    4.33 +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    4.34 +fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    4.35 +
    4.36  end;