--- a/src/HOL/Tools/ATP_Manager/async_manager.ML Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Fri Jun 25 18:34:06 2010 +0200
@@ -8,9 +8,9 @@
signature ASYNC_MANAGER =
sig
- val unregister : bool -> string -> Thread.thread -> unit
- val register :
- string -> bool -> Time.time -> Time.time -> Thread.thread * string -> unit
+ val launch :
+ string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
+ -> unit
val kill_threads : string -> unit
val running_threads : string -> unit
val thread_messages : string -> int option -> unit
@@ -158,7 +158,7 @@
(* register thread *)
-fun register tool verbose birth_time death_time (thread, desc) =
+fun register tool verbose birth_time death_time desc thread =
(Synchronized.change global_state
(fn {manager, timeout_heap, active, canceling, messages, store} =>
let
@@ -169,6 +169,16 @@
check_thread_manager tool verbose);
+fun launch tool verbose birth_time death_time desc f =
+ (Toplevel.thread true
+ (fn () =>
+ let
+ val self = Thread.self ()
+ val _ = register tool verbose birth_time death_time desc self
+ val message = f ()
+ in unregister verbose message self end);
+ ())
+
(** user commands **)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 18:34:06 2010 +0200
@@ -56,9 +56,9 @@
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover
val available_atps: theory -> unit
- val start_prover_thread:
- params -> Time.time -> Time.time -> int -> int -> relevance_override
- -> (string -> minimize_command) -> Proof.state -> string -> unit
+ val start_prover_thread :
+ params -> int -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> string -> unit
end;
structure ATP_Manager : ATP_MANAGER =
@@ -67,13 +67,12 @@
open Metis_Clauses
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
-open Async_Manager
(** The Sledgehammer **)
-fun kill_atps () = kill_threads "ATPs"
-fun running_atps () = running_threads "ATPs"
-val messages = thread_messages "ATP"
+fun kill_atps () = Async_Manager.kill_threads "ATPs"
+fun running_atps () = Async_Manager.running_threads "ATPs"
+val messages = Async_Manager.thread_messages "ATP"
(** problems, results, provers, etc. **)
@@ -145,29 +144,29 @@
(* start prover thread *)
-fun start_prover_thread (params as {verbose, full_types, timeout, ...})
- birth_time death_time i n relevance_override
- minimize_command proof_state name =
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+ relevance_override minimize_command proof_state name =
let
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
val prover = get_prover (Proof.theory_of proof_state) name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
- val _ = Toplevel.thread true (fn () =>
- let
- val _ = register "Sledgehammer" verbose birth_time death_time
- (Thread.self (), desc)
- val problem =
- {subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
- val message =
- #message (prover params (minimize_command name) timeout problem)
- handle TRIVIAL () => metis_line full_types i n []
- | ERROR message => "Error: " ^ message ^ "\n"
- val _ = unregister verbose message (Thread.self ());
- in () end)
- in () end
+ in
+ Async_Manager.launch "Sledgehammer" verbose birth_time death_time desc
+ (fn () =>
+ let
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ in
+ prover params (minimize_command name) timeout problem |> #message
+ handle TRIVIAL () => metis_line full_types i n []
+ | ERROR message => "Error: " ^ message ^ "\n"
+ end)
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Jun 25 18:34:06 2010 +0200
@@ -25,8 +25,8 @@
val is_theorem_bad_for_atps: thm -> bool
val type_has_topsort: typ -> bool
val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
- val saturate_skolem_cache: theory -> theory option
- val auto_saturate_skolem_cache: bool Unsynchronized.ref
+ val saturate_cache: theory -> theory option
+ val auto_saturate_cache: bool Unsynchronized.ref
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -504,7 +504,7 @@
in
-fun saturate_skolem_cache thy =
+fun saturate_cache thy =
let
val facts = PureThy.facts_of thy;
val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
@@ -536,10 +536,10 @@
end;
(* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_skolem_cache = Unsynchronized.ref true
+val auto_saturate_cache = Unsynchronized.ref true
-fun conditionally_saturate_skolem_cache thy =
- if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
+fun conditionally_saturate_cache thy =
+ if !auto_saturate_cache then saturate_cache thy else NONE
(*** Converting a subgoal into negated conjecture clauses. ***)
@@ -565,7 +565,7 @@
(** setup **)
val setup =
- perhaps conditionally_saturate_skolem_cache
- #> Theory.at_end conditionally_saturate_skolem_cache
+ perhaps conditionally_saturate_cache
+ #> Theory.at_end conditionally_saturate_cache
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 18:34:06 2010 +0200
@@ -199,13 +199,10 @@
0 => priority "No subgoal!"
| n =>
let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
val _ = kill_atps ()
val _ = priority "Sledgehammering..."
- val _ = app (start_prover_thread params birth_time death_time i n
- relevance_override minimize_command
- state) atps
+ val _ = app (start_prover_thread params i n relevance_override
+ minimize_command state) atps
in () end
fun minimize override_params i refs state =