# HG changeset patch # User blanchet # Date 1271495122 -7200 # Node ID d4b494b7f1a1c21a52b3596d44734fcbf128a89f # Parent 2db3711b2b032db15df5e0d77be07678c0582aee# Parent 500fc43d5537585d49ca37512d60302aa50cb74a merged diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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 diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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)); diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 *) diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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; diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 2db3711b2b03 -r d4b494b7f1a1 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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))