merged
authorblanchet
Wed, 14 Apr 2010 21:22:48 +0200
changeset 36144 e8db171b8643
parent 36139 0c2538afe8e8 (current diff)
parent 36143 6490319b1703 (diff)
child 36145 42d690c1cd31
child 36167 c1a35be8e476
merged
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:48 2010 +0200
@@ -12,6 +12,7 @@
   type params =
     {debug: bool,
      verbose: bool,
+     overlord: bool,
      atps: string list,
      full_types: bool,
      respect_no_atp: bool,
@@ -64,6 +65,7 @@
 type params =
   {debug: bool,
    verbose: bool,
+   overlord: bool,
    atps: string list,
    full_types: bool,
    respect_no_atp: bool,
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 21:22:48 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,11 +115,12 @@
 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
+    val {context = ctxt, facts, goal} = Proof.raw_goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},
@@ -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)
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 21:22:48 2010 +0200
@@ -65,8 +65,8 @@
           else SOME "Ill-formed ATP output"
   | (failure :: _) => SOME failure
 
-fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
-        name ({full_types, ...} : params)
+fun generic_prover overlord get_facts prepare write cmd args failure_strs
+        produce_answer name ({full_types, ...} : params)
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -87,11 +87,15 @@
       prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
 
     (* path to unique problem file *)
-    val destdir' = Config.get ctxt destdir;
+    val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
+                   else Config.get ctxt destdir;
     val problem_prefix' = Config.get ctxt problem_prefix;
     fun prob_pathname nr =
-      let val probfile =
-        Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
+      let
+        val probfile =
+          Path.basic (problem_prefix' ^
+                      (if overlord then "_" ^ name else serial_string ())
+                      ^ "_" ^ string_of_int nr)
       in
         if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode destdir')
@@ -159,11 +163,11 @@
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
                 prefers_theory_const, supports_isar_proofs})
-        (params as {respect_no_atp, relevance_threshold, convergence,
+        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_const, higher_order, follow_defs, isar_proof,
                     modulus, sorts, ...})
         timeout =
-  generic_prover
+  generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_const theory_const))
@@ -179,6 +183,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 +192,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 +207,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",
@@ -217,10 +223,10 @@
 fun generic_dfg_prover
         (name, ({command, arguments, failure_strs, max_new_clauses,
                  prefers_theory_const, ...} : prover_config))
-        (params as {respect_no_atp, relevance_threshold, convergence,
+        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_const, higher_order, follow_defs, ...})
         timeout =
-  generic_prover
+  generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_const theory_const))
@@ -233,7 +239,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 +282,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,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 21:22:48 2010 +0200
@@ -40,6 +40,7 @@
 val default_default_params =
   [("debug", "false"),
    ("verbose", "false"),
+   ("overlord", "false"),
    ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
    ("convergence", "320"),
@@ -51,9 +52,12 @@
    ("sorts", "false"),
    ("minimize_timeout", "5 s")]
 
-val negated_params =
+val alias_params =
+  [("atp", "atps")]
+val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),
+   ("no_overlord", "overlord"),
    ("ignore_no_atp", "respect_no_atp"),
    ("partial_types", "full_types"),
    ("no_theory_const", "theory_const"),
@@ -66,21 +70,25 @@
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
-  AList.defined (op =) negated_params s orelse
+  AList.defined (op =) alias_params s orelse
+  AList.defined (op =) negated_alias_params s orelse
   member (op =) property_dependent_params s
 
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
   else error ("Unknown parameter: " ^ quote s ^ ".")
 
-fun unnegate_raw_param (name, value) =
-  case AList.lookup (op =) negated_params name of
-    SOME name' => (name', case value of
-                            ["false"] => ["true"]
-                          | ["true"] => ["false"]
-                          | [] => ["false"]
-                          | _ => value)
-  | NONE => (name, value)
+fun unalias_raw_param (name, value) =
+  case AList.lookup (op =) alias_params name of
+    SOME name' => (name', value)
+  | NONE =>
+    case AList.lookup (op =) negated_alias_params name of
+      SOME name' => (name', case value of
+                              ["false"] => ["true"]
+                            | ["true"] => ["false"]
+                            | [] => ["false"]
+                            | _ => value)
+    | NONE => (name, value)
 
 structure Data = Theory_Data(
   type T = raw_param list
@@ -88,19 +96,23 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params thy =
-  [("atps", [!atps]),
-   ("full_types", [if !full_types then "true" else "false"]),
-   ("timeout", [string_of_int (!timeout) ^ " s"])] @
   Data.get thy
+  |> fold (AList.default (op =))
+          [("atps", [!atps]),
+           ("full_types", [if !full_types then "true" else "false"]),
+           ("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)
 
 fun extract_params thy default_params override_params =
   let
-    val override_params = map unnegate_raw_param override_params
+    val override_params = map unalias_raw_param override_params
     val raw_params = rev override_params @ rev default_params
     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
     val lookup_string = the_default "" o lookup
@@ -123,6 +135,7 @@
                                    " must be assigned an integer value.")
     val debug = lookup_bool "debug"
     val verbose = debug orelse lookup_bool "verbose"
+    val overlord = lookup_bool "overlord"
     val atps = lookup_string "atps" |> space_explode " "
     val full_types = lookup_bool "full_types"
     val respect_no_atp = lookup_bool "respect_no_atp"
@@ -138,18 +151,18 @@
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
-    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
-     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
-     convergence = convergence, theory_const = theory_const,
-     higher_order = higher_order, follow_defs = follow_defs,
-     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
-     timeout = timeout, minimize_timeout = minimize_timeout}
+    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
+     full_types = full_types, respect_no_atp = respect_no_atp,
+     relevance_threshold = relevance_threshold, convergence = convergence,
+     theory_const = theory_const, higher_order = higher_order,
+     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
+     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
-fun atp_minimize_command override_params old_style_args i fact_refs state =
+fun minimize override_params old_style_args i fact_refs state =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -174,7 +187,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
@@ -198,6 +211,9 @@
 val delN = "del"
 val onlyN = "only"
 
+fun minimizize_raw_param_name "timeout" = "minimize_timeout"
+  | minimizize_raw_param_name name = name
+
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val thy = Proof.theory_of state
@@ -207,8 +223,8 @@
       sledgehammer (get_params thy override_params) (the_default 1 opt_i)
                    relevance_override state
     else if subcommand = minimizeN then
-      atp_minimize_command override_params [] (the_default 1 opt_i)
-                           (#add relevance_override) state
+      minimize (map (apfst minimizize_raw_param_name) override_params) []
+               (the_default 1 opt_i) (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_atpsN then
@@ -293,8 +309,7 @@
     "minimize theorem list with external prover" K.diag
     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
       Toplevel.no_timing o Toplevel.unknown_proof o
-        Toplevel.keep (atp_minimize_command [] args 1 fact_refs
-                       o Toplevel.proof_of)))
+        Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
 
 val _ =
   OuterSyntax.improper_command "sledgehammer"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 21:22:48 2010 +0200
@@ -550,7 +550,7 @@
   | minimize_line name xs =
       "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback
-                    ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+                    ("sledgehammer minimize [atp = " ^ name ^ "] (" ^
                      space_implode " " xs ^ ")") ^ ".\n"
 
 fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 19:46:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 21:22:48 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;