--- 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;