merged
authorblanchet
Wed Apr 14 21:22:48 2010 +0200 (2010-04-14)
changeset 36144e8db171b8643
parent 36139 0c2538afe8e8
parent 36143 6490319b1703
child 36145 42d690c1cd31
child 36167 c1a35be8e476
merged
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 19:46:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:48 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    type params =
     1.5      {debug: bool,
     1.6       verbose: bool,
     1.7 +     overlord: bool,
     1.8       atps: string list,
     1.9       full_types: bool,
    1.10       respect_no_atp: bool,
    1.11 @@ -64,6 +65,7 @@
    1.12  type params =
    1.13    {debug: bool,
    1.14     verbose: bool,
    1.15 +   overlord: bool,
    1.16     atps: string list,
    1.17     full_types: bool,
    1.18     respect_no_atp: bool,
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 19:46:36 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 21:22:48 2010 +0200
     2.3 @@ -22,6 +22,7 @@
     2.4  structure ATP_Minimal : ATP_MINIMAL =
     2.5  struct
     2.6  
     2.7 +open Sledgehammer_Util
     2.8  open Sledgehammer_Fact_Preprocessor
     2.9  open Sledgehammer_Proof_Reconstruct
    2.10  open ATP_Manager
    2.11 @@ -114,11 +115,12 @@
    2.12  fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
    2.13          timeout subgoal state filtered name_thms_pairs =
    2.14    let
    2.15 -    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
    2.16 -                      " theorems... ")
    2.17 +    val num_theorems = length name_thms_pairs
    2.18 +    val _ = priority ("Testing " ^ string_of_int num_theorems ^
    2.19 +                      " theorem" ^ plural_s num_theorems ^ "...")
    2.20      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    2.21      val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    2.22 -    val {context = ctxt, facts, goal} = Proof.goal state
    2.23 +    val {context = ctxt, facts, goal} = Proof.raw_goal state
    2.24      val problem =
    2.25       {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    2.26        relevance_override = {add = [], del = [], only = false},
    2.27 @@ -161,12 +163,17 @@
    2.28              ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
    2.29          in (SOME min_thms, metis_line i n min_names) end
    2.30      | (Timeout, _) =>
    2.31 -        (NONE, "Timeout: You may need to increase the time limit of " ^
    2.32 -          string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
    2.33 +        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
    2.34 +               \option (e.g., \"timeout = " ^
    2.35 +               string_of_int (10 + msecs div 1000) ^ " s\").")
    2.36      | (Error, msg) =>
    2.37          (NONE, "Error in prover: " ^ msg)
    2.38      | (Failure, _) =>
    2.39 -        (NONE, "Failure: No proof with the theorems supplied"))
    2.40 +        (* Failure sometimes mean timeout, unfortunately. *)
    2.41 +        (NONE, "Failure: No proof was found with the current time limit. You \
    2.42 +               \can increase the time limit using the \"timeout\" \
    2.43 +               \option (e.g., \"timeout = " ^
    2.44 +               string_of_int (10 + msecs div 1000) ^ " s\")."))
    2.45      handle Sledgehammer_HOL_Clause.TRIVIAL =>
    2.46          (SOME [], metis_line i n [])
    2.47        | ERROR msg => (NONE, "Error: " ^ msg)
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 19:46:36 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 21:22:48 2010 +0200
     3.3 @@ -65,8 +65,8 @@
     3.4            else SOME "Ill-formed ATP output"
     3.5    | (failure :: _) => SOME failure
     3.6  
     3.7 -fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
     3.8 -        name ({full_types, ...} : params)
     3.9 +fun generic_prover overlord get_facts prepare write cmd args failure_strs
    3.10 +        produce_answer name ({full_types, ...} : params)
    3.11          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    3.12           : problem) =
    3.13    let
    3.14 @@ -87,11 +87,15 @@
    3.15        prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
    3.16  
    3.17      (* path to unique problem file *)
    3.18 -    val destdir' = Config.get ctxt destdir;
    3.19 +    val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
    3.20 +                   else Config.get ctxt destdir;
    3.21      val problem_prefix' = Config.get ctxt problem_prefix;
    3.22      fun prob_pathname nr =
    3.23 -      let val probfile =
    3.24 -        Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
    3.25 +      let
    3.26 +        val probfile =
    3.27 +          Path.basic (problem_prefix' ^
    3.28 +                      (if overlord then "_" ^ name else serial_string ())
    3.29 +                      ^ "_" ^ string_of_int nr)
    3.30        in
    3.31          if destdir' = "" then File.tmp_path probfile
    3.32          else if File.exists (Path.explode destdir')
    3.33 @@ -159,11 +163,11 @@
    3.34  fun generic_tptp_prover
    3.35          (name, {command, arguments, failure_strs, max_new_clauses,
    3.36                  prefers_theory_const, supports_isar_proofs})
    3.37 -        (params as {respect_no_atp, relevance_threshold, convergence,
    3.38 +        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    3.39                      theory_const, higher_order, follow_defs, isar_proof,
    3.40                      modulus, sorts, ...})
    3.41          timeout =
    3.42 -  generic_prover
    3.43 +  generic_prover overlord
    3.44        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.45                            higher_order follow_defs max_new_clauses
    3.46                            (the_default prefers_theory_const theory_const))
    3.47 @@ -179,6 +183,8 @@
    3.48  
    3.49  (** common provers **)
    3.50  
    3.51 +fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
    3.52 +
    3.53  (* Vampire *)
    3.54  
    3.55  (* NB: Vampire does not work without explicit time limit. *)
    3.56 @@ -186,7 +192,7 @@
    3.57  val vampire_config : prover_config =
    3.58    {command = Path.explode "$VAMPIRE_HOME/vampire",
    3.59     arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
    3.60 -                              string_of_int (Time.toSeconds timeout)),
    3.61 +                              string_of_int (generous_to_secs timeout)),
    3.62     failure_strs =
    3.63       ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
    3.64     max_new_clauses = 60,
    3.65 @@ -201,7 +207,7 @@
    3.66    {command = Path.explode "$E_HOME/eproof",
    3.67     arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
    3.68                                \-tAutoDev --silent --cpu-limit=" ^
    3.69 -                              string_of_int (Time.toSeconds timeout)),
    3.70 +                              string_of_int (generous_to_secs timeout)),
    3.71     failure_strs =
    3.72         ["SZS status: Satisfiable", "SZS status Satisfiable",
    3.73          "SZS status: ResourceOut", "SZS status ResourceOut",
    3.74 @@ -217,10 +223,10 @@
    3.75  fun generic_dfg_prover
    3.76          (name, ({command, arguments, failure_strs, max_new_clauses,
    3.77                   prefers_theory_const, ...} : prover_config))
    3.78 -        (params as {respect_no_atp, relevance_threshold, convergence,
    3.79 +        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    3.80                      theory_const, higher_order, follow_defs, ...})
    3.81          timeout =
    3.82 -  generic_prover
    3.83 +  generic_prover overlord
    3.84        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.85                            higher_order follow_defs max_new_clauses
    3.86                            (the_default prefers_theory_const theory_const))
    3.87 @@ -233,7 +239,7 @@
    3.88   {command = Path.explode "$SPASS_HOME/SPASS",
    3.89    arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
    3.90      " -FullRed=0 -DocProof -TimeLimit=" ^
    3.91 -    string_of_int (Time.toSeconds timeout)),
    3.92 +    string_of_int (generous_to_secs timeout)),
    3.93    failure_strs =
    3.94      ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
    3.95       "SPASS beiseite: Maximal number of loops exceeded."],
    3.96 @@ -276,7 +282,7 @@
    3.97           : prover_config) : prover_config =
    3.98    {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    3.99     arguments = (fn timeout =>
   3.100 -     args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
   3.101 +     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
   3.102       the_system prover_prefix),
   3.103     failure_strs = remote_failure_strs @ failure_strs,
   3.104     max_new_clauses = max_new_clauses,
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 19:46:36 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 21:22:48 2010 +0200
     4.3 @@ -40,6 +40,7 @@
     4.4  val default_default_params =
     4.5    [("debug", "false"),
     4.6     ("verbose", "false"),
     4.7 +   ("overlord", "false"),
     4.8     ("respect_no_atp", "true"),
     4.9     ("relevance_threshold", "50"),
    4.10     ("convergence", "320"),
    4.11 @@ -51,9 +52,12 @@
    4.12     ("sorts", "false"),
    4.13     ("minimize_timeout", "5 s")]
    4.14  
    4.15 -val negated_params =
    4.16 +val alias_params =
    4.17 +  [("atp", "atps")]
    4.18 +val negated_alias_params =
    4.19    [("no_debug", "debug"),
    4.20     ("quiet", "verbose"),
    4.21 +   ("no_overlord", "overlord"),
    4.22     ("ignore_no_atp", "respect_no_atp"),
    4.23     ("partial_types", "full_types"),
    4.24     ("no_theory_const", "theory_const"),
    4.25 @@ -66,21 +70,25 @@
    4.26  
    4.27  fun is_known_raw_param s =
    4.28    AList.defined (op =) default_default_params s orelse
    4.29 -  AList.defined (op =) negated_params s orelse
    4.30 +  AList.defined (op =) alias_params s orelse
    4.31 +  AList.defined (op =) negated_alias_params s orelse
    4.32    member (op =) property_dependent_params s
    4.33  
    4.34  fun check_raw_param (s, _) =
    4.35    if is_known_raw_param s then ()
    4.36    else error ("Unknown parameter: " ^ quote s ^ ".")
    4.37  
    4.38 -fun unnegate_raw_param (name, value) =
    4.39 -  case AList.lookup (op =) negated_params name of
    4.40 -    SOME name' => (name', case value of
    4.41 -                            ["false"] => ["true"]
    4.42 -                          | ["true"] => ["false"]
    4.43 -                          | [] => ["false"]
    4.44 -                          | _ => value)
    4.45 -  | NONE => (name, value)
    4.46 +fun unalias_raw_param (name, value) =
    4.47 +  case AList.lookup (op =) alias_params name of
    4.48 +    SOME name' => (name', value)
    4.49 +  | NONE =>
    4.50 +    case AList.lookup (op =) negated_alias_params name of
    4.51 +      SOME name' => (name', case value of
    4.52 +                              ["false"] => ["true"]
    4.53 +                            | ["true"] => ["false"]
    4.54 +                            | [] => ["false"]
    4.55 +                            | _ => value)
    4.56 +    | NONE => (name, value)
    4.57  
    4.58  structure Data = Theory_Data(
    4.59    type T = raw_param list
    4.60 @@ -88,19 +96,23 @@
    4.61    val extend = I
    4.62    fun merge p : T = AList.merge (op =) (K true) p)
    4.63  
    4.64 -val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
    4.65 +val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
    4.66  fun default_raw_params thy =
    4.67 -  [("atps", [!atps]),
    4.68 -   ("full_types", [if !full_types then "true" else "false"]),
    4.69 -   ("timeout", [string_of_int (!timeout) ^ " s"])] @
    4.70    Data.get thy
    4.71 +  |> fold (AList.default (op =))
    4.72 +          [("atps", [!atps]),
    4.73 +           ("full_types", [if !full_types then "true" else "false"]),
    4.74 +           ("timeout", let val timeout = !timeout in
    4.75 +                         [if timeout <= 0 then "none"
    4.76 +                          else string_of_int timeout ^ " s"]
    4.77 +                       end)]
    4.78  
    4.79  val infinity_time_in_secs = 60 * 60 * 24 * 365
    4.80  val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
    4.81  
    4.82  fun extract_params thy default_params override_params =
    4.83    let
    4.84 -    val override_params = map unnegate_raw_param override_params
    4.85 +    val override_params = map unalias_raw_param override_params
    4.86      val raw_params = rev override_params @ rev default_params
    4.87      val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
    4.88      val lookup_string = the_default "" o lookup
    4.89 @@ -123,6 +135,7 @@
    4.90                                     " must be assigned an integer value.")
    4.91      val debug = lookup_bool "debug"
    4.92      val verbose = debug orelse lookup_bool "verbose"
    4.93 +    val overlord = lookup_bool "overlord"
    4.94      val atps = lookup_string "atps" |> space_explode " "
    4.95      val full_types = lookup_bool "full_types"
    4.96      val respect_no_atp = lookup_bool "respect_no_atp"
    4.97 @@ -138,18 +151,18 @@
    4.98      val timeout = lookup_time "timeout"
    4.99      val minimize_timeout = lookup_time "minimize_timeout"
   4.100    in
   4.101 -    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
   4.102 -     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
   4.103 -     convergence = convergence, theory_const = theory_const,
   4.104 -     higher_order = higher_order, follow_defs = follow_defs,
   4.105 -     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
   4.106 -     timeout = timeout, minimize_timeout = minimize_timeout}
   4.107 +    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
   4.108 +     full_types = full_types, respect_no_atp = respect_no_atp,
   4.109 +     relevance_threshold = relevance_threshold, convergence = convergence,
   4.110 +     theory_const = theory_const, higher_order = higher_order,
   4.111 +     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
   4.112 +     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
   4.113    end
   4.114  
   4.115  fun get_params thy = extract_params thy (default_raw_params thy)
   4.116  fun default_params thy = get_params thy o map (apsnd single)
   4.117  
   4.118 -fun atp_minimize_command override_params old_style_args i fact_refs state =
   4.119 +fun minimize override_params old_style_args i fact_refs state =
   4.120    let
   4.121      val thy = Proof.theory_of state
   4.122      val ctxt = Proof.context_of state
   4.123 @@ -174,7 +187,7 @@
   4.124        get_params thy
   4.125            [("atps", [atp]),
   4.126             ("minimize_timeout",
   4.127 -            [string_of_int (Time.toSeconds timeout) ^ " s"])]
   4.128 +            [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]
   4.129      val prover =
   4.130        (case get_prover thy atp of
   4.131          SOME prover => prover
   4.132 @@ -198,6 +211,9 @@
   4.133  val delN = "del"
   4.134  val onlyN = "only"
   4.135  
   4.136 +fun minimizize_raw_param_name "timeout" = "minimize_timeout"
   4.137 +  | minimizize_raw_param_name name = name
   4.138 +
   4.139  fun hammer_away override_params subcommand opt_i relevance_override state =
   4.140    let
   4.141      val thy = Proof.theory_of state
   4.142 @@ -207,8 +223,8 @@
   4.143        sledgehammer (get_params thy override_params) (the_default 1 opt_i)
   4.144                     relevance_override state
   4.145      else if subcommand = minimizeN then
   4.146 -      atp_minimize_command override_params [] (the_default 1 opt_i)
   4.147 -                           (#add relevance_override) state
   4.148 +      minimize (map (apfst minimizize_raw_param_name) override_params) []
   4.149 +               (the_default 1 opt_i) (#add relevance_override) state
   4.150      else if subcommand = messagesN then
   4.151        messages opt_i
   4.152      else if subcommand = available_atpsN then
   4.153 @@ -293,8 +309,7 @@
   4.154      "minimize theorem list with external prover" K.diag
   4.155      (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
   4.156        Toplevel.no_timing o Toplevel.unknown_proof o
   4.157 -        Toplevel.keep (atp_minimize_command [] args 1 fact_refs
   4.158 -                       o Toplevel.proof_of)))
   4.159 +        Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
   4.160  
   4.161  val _ =
   4.162    OuterSyntax.improper_command "sledgehammer"
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 19:46:36 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 21:22:48 2010 +0200
     5.3 @@ -550,7 +550,7 @@
     5.4    | minimize_line name xs =
     5.5        "To minimize the number of lemmas, try this command: " ^
     5.6        Markup.markup Markup.sendback
     5.7 -                    ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
     5.8 +                    ("sledgehammer minimize [atp = " ^ name ^ "] (" ^
     5.9                       space_implode " " xs ^ ")") ^ ".\n"
    5.10  
    5.11  fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 19:46:36 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 14 21:22:48 2010 +0200
     6.3 @@ -6,6 +6,7 @@
     6.4  
     6.5  signature SLEDGEHAMMER_UTIL =
     6.6  sig
     6.7 +  val plural_s : int -> string
     6.8    val serial_commas : string -> string list -> string list
     6.9    val parse_bool_option : bool -> string -> string -> bool option
    6.10    val parse_time_option : string -> string -> Time.time option
    6.11 @@ -17,12 +18,7 @@
    6.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    6.13  struct
    6.14  
    6.15 -(* This hash function is recommended in Compilers: Principles, Techniques, and
    6.16 -   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    6.17 -   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    6.18 -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    6.19 -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    6.20 -fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    6.21 +fun plural_s n = if n = 1 then "" else "s"
    6.22  
    6.23  fun serial_commas _ [] = ["??"]
    6.24    | serial_commas _ [s] = [s]
    6.25 @@ -60,4 +56,11 @@
    6.26          SOME (Time.fromMilliseconds msecs)
    6.27      end
    6.28  
    6.29 +(* This hash function is recommended in Compilers: Principles, Techniques, and
    6.30 +   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    6.31 +   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    6.32 +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    6.33 +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    6.34 +fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    6.35 +
    6.36  end;