--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Apr 17 11:05:22 2010 +0200
@@ -160,14 +160,22 @@
(* unregister ATP thread *)
-fun unregister message thread = Synchronized.change global_state
+fun unregister ({verbose, ...} : params) message thread =
+ Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
- SOME (_, _, description) =>
+ SOME (birth_time, _, description) =>
let
val active' = delete_thread thread active;
- val cancelling' = (thread, (Time.now (), description)) :: cancelling;
- val message' = description ^ "\n" ^ message;
+ val now = Time.now ()
+ val cancelling' = (thread, (now, description)) :: cancelling;
+ val message' =
+ description ^ "\n" ^ message ^
+ (if verbose then
+ "Total time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms.\n"
+ else
+ "")
val messages' = message' :: messages;
val store' = message' ::
(if length store <= message_store_limit then store
@@ -190,7 +198,7 @@
else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
end;
-fun check_thread_manager () = Synchronized.change global_state
+fun check_thread_manager params = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
else let val manager = SOME (Toplevel.thread false (fn () =>
@@ -223,7 +231,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister "Timed out.");
+ |> List.app (unregister params "Timed out.");
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
@@ -233,7 +241,7 @@
(* register ATP thread *)
-fun register birth_time death_time (thread, desc) =
+fun register params birth_time death_time (thread, desc) =
(Synchronized.change global_state
(fn {manager, timeout_heap, active, cancelling, messages, store} =>
let
@@ -241,7 +249,7 @@
val active' = update_thread (thread, (birth_time, death_time, desc)) active;
val state' = make_state manager timeout_heap' active' cancelling messages store;
in state' end);
- check_thread_manager ());
+ check_thread_manager params);
@@ -325,7 +333,7 @@
fun start_prover (params as {timeout, ...}) birth_time death_time i
relevance_override proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
- NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
+ NONE => warning ("Unknown ATP: " ^ quote name)
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -336,7 +344,7 @@
val _ = Toplevel.thread true (fn () =>
let
- val _ = register birth_time death_time (Thread.self (), desc);
+ val _ = register params birth_time death_time (Thread.self (), desc)
val problem =
{subgoal = i, goal = (ctxt, (facts, goal)),
relevance_override = relevance_override, axiom_clauses = NONE,
@@ -345,7 +353,7 @@
handle Sledgehammer_HOL_Clause.TRIVIAL =>
metis_line i n []
| ERROR msg => ("Error: " ^ msg);
- val _ = unregister message (Thread.self ());
+ val _ = unregister params message (Thread.self ());
in () end);
in () end);
@@ -357,10 +365,7 @@
let
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val _ =
- (* RACE w.r.t. other invocations of Sledgehammer *)
- if null (#active (Synchronized.value global_state)) then ()
- else (kill_atps (); priority "Killed active Sledgehammer threads.")
+ val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
val _ = priority "Sledgehammering..."
val _ = List.app (start_prover params birth_time death_time i
relevance_override proof_state) atps
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sat Apr 17 11:05:22 2010 +0200
@@ -20,6 +20,7 @@
structure ATP_Wrapper : ATP_WRAPPER =
struct
+open Sledgehammer_Util
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
@@ -135,8 +136,11 @@
the proof file too. *)
fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
fun export probfile (((proof, _), _), _) =
- if destdir' = "" then ()
- else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
+ if destdir' = "" then
+ ()
+ else
+ File.write (Path.explode (Path.implode probfile ^ "_proof"))
+ ("% " ^ timestamp () ^ "\n" ^ proof)
val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
@@ -145,8 +149,8 @@
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
val (message, relevant_thm_names) =
- if is_some failure then ("ATP failed to find a proof.", [])
- else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
+ if is_some failure then ("ATP failed to find a proof.\n", [])
+ else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
else
(produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
subgoal));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Apr 17 11:05:22 2010 +0200
@@ -177,9 +177,8 @@
(*The frequency of a constant is the sum of those of all instances of its type.*)
fun const_frequency ctab (c, cts) =
- let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
- fun add ((cts',m), n) = if match_types cts cts' then m+n else n
- in List.foldl add 0 pairs end;
+ CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
+ (the (Symtab.lookup ctab c)) 0
(*Add in a constant's weight, as determined by its frequency.*)
fun add_ct_weight ctab ((c,T), w) =
@@ -253,40 +252,46 @@
end;
fun relevant_clauses ctxt convergence follow_defs max_new
- (relevance_override as {add, del, only}) thy ctab p
- rel_consts =
- let val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
- | relevant (newpairs,rejects) [] =
- let val (newrels,more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
- val newp = p + (1.0-p) / convergence
+ (relevance_override as {add, del, only}) thy ctab =
+ let
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter p rel_consts =
+ let
+ fun relevant ([], _) [] = [] (* Nothing added this iteration *)
+ | relevant (newpairs,rejects) [] =
+ let
+ val (newrels, more_rejects) = take_best max_new newpairs
+ val new_consts = maps #2 newrels
+ val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
+ val newp = p + (1.0-p) / convergence
in
- trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
- map #1 newrels @
- relevant_clauses ctxt convergence follow_defs max_new
- relevance_override thy ctab newp rel_consts'
- (more_rejects @ rejects)
+ trace_msg (fn () => "relevant this iteration: " ^
+ Int.toString (length newrels));
+ map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects)
end
- | relevant (newrels, rejects)
- ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+ | relevant (newrels, rejects)
+ ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
let
val weight = if member Thm.eq_thm del_thms thm then 0.0
else if member Thm.eq_thm add_thms thm then 1.0
else if only then 0.0
else clause_weight ctab rel_consts consts_typs
in
- if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
- then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight));
- relevant ((ax,weight)::newrels, rejects) axs)
- else relevant (newrels, ax::rejects) axs
+ if p <= weight orelse
+ (follow_defs andalso defines thy (#1 clsthm) rel_consts) then
+ (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight);
+ relevant ((ax, weight) :: newrels, rejects) axs)
+ else
+ relevant (newrels, ax :: rejects) axs
end
- in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
- relevant ([],[])
- end;
+ in
+ trace_msg (fn () => "relevant_clauses, current pass mark: " ^
+ Real.toString p);
+ relevant ([], [])
+ end
+ in iter end
fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
theory_const relevance_override thy axioms goals =
@@ -498,19 +503,23 @@
fun get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new theory_const
- relevance_override (ctxt, (chain_ths, th)) goal_cls =
- let
- val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy higher_order goal_cls
- val included_cls = get_all_lemmas respect_no_atp ctxt
- |> cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy is_FO
- |> remove_unwanted_clauses
- in
- relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_const relevance_override thy included_cls
- (map prop_of goal_cls)
- end;
+ (relevance_override as {add, only, ...})
+ (ctxt, (chain_ths, th)) goal_cls =
+ if (only andalso null add) orelse relevance_threshold > 1.0 then
+ []
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ val is_FO = is_first_order thy higher_order goal_cls
+ val included_cls = get_all_lemmas respect_no_atp ctxt
+ |> cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy is_FO
+ |> remove_unwanted_clauses
+ in
+ relevance_filter ctxt relevance_threshold convergence follow_defs max_new
+ theory_const relevance_override thy included_cls
+ (map prop_of goal_cls)
+ end
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sat Apr 17 11:05:22 2010 +0200
@@ -502,10 +502,10 @@
"% " ^ timestamp () ^ "\n" ::
section "Relevant fact" ax_clss @
section "Type variable" tfree_clss @
+ section "Conjecture" conjecture_clss @
section "Class relationship" classrel_clss @
section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss @
- section "Conjecture" conjecture_clss)
+ section "Helper fact" helper_clss)
in (length axclauses + 1, length tfree_clss + length conjecture_clss)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 17 11:05:22 2010 +0200
@@ -27,13 +27,13 @@
{add = [], del = ns, only = false}
fun only_relevance_override ns : relevance_override =
{add = ns, del = [], only = true}
-val default_relevance_override = add_to_relevance_override []
+val no_relevance_override = add_to_relevance_override []
fun merge_relevance_override_pairwise (r1 : relevance_override)
(r2 : relevance_override) =
{add = #add r1 @ #add r2, del = #del r1 @ #del r2,
- only = #only r1 orelse #only r2}
+ only = #only r1 andalso #only r2}
fun merge_relevance_overrides rs =
- fold merge_relevance_override_pairwise rs default_relevance_override
+ fold merge_relevance_override_pairwise rs (only_relevance_override [])
type raw_param = string * string list
@@ -96,11 +96,19 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
+(* Don't even try to start ATPs that are not installed.
+ Hack: Should not rely on naming convention. *)
+val filter_atps =
+ space_explode " "
+ #> filter (fn s => String.isPrefix "remote_" s orelse
+ getenv (String.map Char.toUpper s ^ "_HOME") <> "")
+ #> space_implode " "
+
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params thy =
Data.get thy
|> fold (AList.default (op =))
- [("atps", [!atps]),
+ [("atps", [filter_atps (!atps)]),
("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
@@ -207,9 +215,6 @@
val refresh_tptpN = "refresh_tptp"
val helpN = "help"
-val addN = "add"
-val delN = "del"
-val onlyN = "only"
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
| minimizize_raw_param_name name = name
@@ -270,14 +275,11 @@
(Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
|| (Args.del |-- Args.colon |-- parse_fact_refs
>> del_from_relevance_override)
- || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+ || (parse_fact_refs >> only_relevance_override)
val parse_relevance_override =
- Scan.optional (Args.parens
- (Scan.optional (parse_fact_refs >> only_relevance_override)
- default_relevance_override
- -- Scan.repeat parse_relevance_chunk)
- >> op :: >> merge_relevance_overrides)
- default_relevance_override
+ Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
+ >> merge_relevance_overrides))
+ (add_to_relevance_override [])
val parse_sledgehammer_command =
(Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
-- Scan.option P.nat) #>> sledgehammer_trans
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 22:52:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Apr 17 11:05:22 2010 +0200
@@ -33,7 +33,7 @@
let
fun aux seen "" = String.implode (rev seen)
| aux seen s =
- if String.isPrefix bef s then
+ if String.isPrefix bef s then
aux seen "" ^ aft ^ aux [] (unprefix bef s)
else
aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))