--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 18:11:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:12:49 2010 +0200
@@ -8,11 +8,10 @@
signature SLEDGEHAMMER_FACT_MINIMIZER =
sig
type params = ATP_Manager.params
- type prover = ATP_Manager.prover
type prover_result = ATP_Manager.prover_result
val minimize_theorems :
- params -> prover -> string -> int -> Proof.state -> (string * thm list) list
+ params -> int -> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -68,14 +67,18 @@
(* minimalization of thms *)
-fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
- sorts, ...})
- prover atp_name i state name_thms_pairs =
+fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
+ modulus, sorts, ...})
+ i state name_thms_pairs =
let
+ val thy = Proof.theory_of state
+ val prover = case atps of
+ [atp_name] => get_prover thy atp_name
+ | _ => error "Expected a single ATP."
val msecs = Time.toMilliseconds minimize_timeout
val n = length name_thms_pairs
val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
+ priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
val test_thms_fun =
sledgehammer_test_theorems params prover minimize_timeout i state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 23 18:11:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 23 19:12:49 2010 +0200
@@ -190,11 +190,15 @@
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-(* HACK because SPASS 3.0 truncates identifiers to 63 characters. (This is
- solved in 3.7 and perhaps in earlier versions too.) *)
-(* 32-bit hash, so we expect no collisions. *)
+val max_dfg_symbol_length = 63
+
+(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
fun controlled_length dfg s =
- if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s;
+ if dfg andalso size s > max_dfg_symbol_length then
+ String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^
+ String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE)
+ else
+ s
fun lookup_const dfg c =
case Symtab.lookup const_trans_table c of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 18:11:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 19:12:49 2010 +0200
@@ -211,40 +211,16 @@
proof_state) atps
in () end
-fun minimize override_params old_style_args i fact_refs state =
+fun minimize override_params i fact_refs state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- fun theorems_from_refs ctxt =
- map (fn fact_ref =>
- let
- val ths = ProofContext.get_fact ctxt fact_ref
- val name' = Facts.string_of_ref fact_ref
- in (name', ths) end)
- fun get_time_limit_arg s =
- (case Int.fromString s of
- SOME t => Time.fromSeconds t
- | NONE => error ("Invalid time limit: " ^ quote s ^ "."))
- fun get_opt (name, a) (p, t) =
- (case name of
- "time" => (p, get_time_limit_arg a)
- | "atp" => (a, t)
- | n => error ("Invalid argument: " ^ n ^ "."))
- val {atps, minimize_timeout, ...} = get_params thy override_params
- val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
- val params =
- get_params thy
- (override_params @
- [("atps", [atp]),
- ("minimize_timeout",
- [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])
- val prover =
- (case get_prover thy atp of
- SOME prover => prover
- | NONE => error ("Unknown ATP: " ^ quote atp ^ "."))
+ val theorems_from_refs =
+ map o pairf Facts.string_of_ref o ProofContext.get_fact
val name_thms_pairs = theorems_from_refs ctxt fact_refs
in
- priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
+ priority (#2 (minimize_theorems (get_params thy override_params) i state
+ name_thms_pairs))
end
val sledgehammerN = "sledgehammer"
@@ -287,7 +263,7 @@
(minimize_command override_params i) state
end
else if subcommand = minimizeN then
- minimize (map (apfst minimizize_raw_param_name) override_params) []
+ 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
@@ -345,33 +321,6 @@
val parse_sledgehammer_params_command =
parse_params #>> sledgehammer_params_trans
-val parse_minimize_args =
- Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
- []
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
-val _ =
- OuterSyntax.improper_command "atp_info"
- "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
-val _ =
- OuterSyntax.improper_command "atp_messages"
- "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing
- o Toplevel.imperative (fn () => messages limit)))
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (available_atps o Toplevel.theory_of)))
-val _ =
- OuterSyntax.improper_command "atp_minimize"
- "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 (minimize [] args 1 fact_refs o Toplevel.proof_of)))
-
val _ =
OuterSyntax.improper_command sledgehammerN
"search for first-order proof using automatic theorem provers" K.diag
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 23 18:11:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 23 19:12:49 2010 +0200
@@ -6,6 +6,7 @@
signature SLEDGEHAMMER_UTIL =
sig
+ val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val replace_all : string -> string -> string -> string
@@ -13,14 +14,13 @@
val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
- val hashw : word * word -> word
- val hashw_char : Char.char * word -> word
- val hashw_string : string * word -> word
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
+fun pairf f g x = (f x, g x)
+
fun plural_s n = if n = 1 then "" else "s"
fun serial_commas _ [] = ["??"]
@@ -73,11 +73,4 @@
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;