author | wenzelm |
Fri, 03 Oct 2008 20:10:44 +0200 | |
changeset 28487 | 13e637e0c876 |
parent 28484 | 4ed9239b09c1 |
child 28543 | 637f2808ab64 |
permissions | -rw-r--r-- |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/atp_manager.ML |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
3 |
Author: Fabian Immler, TU Muenchen |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
4 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
5 |
ATP threads have to be registered here. Threads with the same |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
6 |
birth-time are seen as one group. All threads of a group are killed |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
7 |
when one thread of it has been successful, or after a certain time, or |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
8 |
when the maximum number of threads exceeds; then the oldest thread is |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
9 |
killed. |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
11 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
12 |
signature ATP_MANAGER = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
13 |
sig |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
14 |
val kill_all: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
15 |
val info: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
16 |
val set_atps: string -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
17 |
val set_max_atp: int -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
18 |
val set_timeout: int -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
19 |
val set_groupkilling: bool -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
20 |
val start: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
21 |
val register: Time.time -> Time.time -> (Thread.thread * string) -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
22 |
val unregister: bool -> unit |
28484 | 23 |
val add_prover: string -> (Proof.state -> Thread.thread * string) -> theory -> theory |
24 |
val print_provers: theory -> unit |
|
25 |
val sledgehammer: Proof.state -> unit |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
26 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
27 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
28 |
structure AtpManager : ATP_MANAGER = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
29 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
30 |
|
28484 | 31 |
structure ThreadHeap = HeapFun |
32 |
( |
|
33 |
type elem = Time.time * Thread.thread; |
|
34 |
fun ord ((a, _), (b, _)) = Time.compare (a, b); |
|
35 |
); |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
36 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
37 |
(* create global state of threadmanager *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
38 |
val timeout_heap = ref ThreadHeap.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
39 |
val oldest_heap = ref ThreadHeap.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
40 |
(* managed threads *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
41 |
val active = ref ([] : (Thread.thread * Time.time * Time.time * string) list) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
42 |
val cancelling = ref ([] : (Thread.thread * Time.time * Time.time * string) list) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
43 |
(* settings *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
44 |
val atps = ref "e,spass" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
45 |
val maximum_atps = ref 5 (* ~1 means infinite number of atps*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
46 |
val timeout = ref 60 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
47 |
val groupkilling = ref true |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
48 |
(* synchronizing *) |
28484 | 49 |
val lock = Mutex.mutex () (* to be acquired for changing state *) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
50 |
val state_change = ConditionVar.conditionVar () (* signal when state changes *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
51 |
(* watches over running threads and interrupts them if required *) |
28478 | 52 |
val managing_thread = ref (NONE: Thread.thread option); |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
53 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
54 |
(* move a thread from active to cancelling |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
55 |
managing_thread trys to interrupt all threads in cancelling |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
56 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
57 |
call from an environment where a lock has already been aquired *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
58 |
fun unregister_locked thread = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
59 |
let val entrys = (filter (fn (t,_,_,_) => Thread.equal (t, thread))) (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
60 |
val entrys_update = map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)) entrys |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
61 |
val _ = change cancelling (append entrys_update) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
62 |
val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
63 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
64 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
65 |
(* start a watching thread which runs forever *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
66 |
(* must *not* be called more than once!! => problem with locks *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
67 |
fun start () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
68 |
let |
28478 | 69 |
val new_thread = SimpleThread.fork false (fn () => |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
70 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
71 |
(* never give up lock except for waiting *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
72 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
73 |
fun wait_for_next_event time = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
74 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
75 |
(* wait for signal or next timeout, give up lock meanwhile *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
76 |
val _ = ConditionVar.waitUntil (state_change, lock, time) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
77 |
(* move threads with priority less than Time.now() to cancelling *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
78 |
fun cancelolder heap = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
79 |
if ThreadHeap.is_empty heap then heap else |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
80 |
let val (mintime, minthread) = ThreadHeap.min heap |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
81 |
in |
28484 | 82 |
if Time.> (mintime, Time.now()) then heap |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
83 |
else (unregister_locked minthread; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
84 |
cancelolder (ThreadHeap.delete_min heap)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
85 |
end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
86 |
val _ = change timeout_heap cancelolder |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
87 |
(* try to interrupt threads that are to cancel*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
88 |
fun interrupt t = Thread.interrupt t handle Thread _ => () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
89 |
val _ = change cancelling (filter (fn (t,_,_,_) => Thread.isActive t)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
90 |
val _ = map (fn (t, _, _, _) => interrupt t) (! cancelling) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
91 |
(* if there are threads to cancel, send periodic interrupts *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
92 |
(* TODO: find out what realtime-values are appropriate *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
93 |
val next_time = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
94 |
if length (! cancelling) > 0 then |
28484 | 95 |
Time.+ (Time.now(), Time.fromMilliseconds 300) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
96 |
else if ThreadHeap.is_empty (! timeout_heap) then |
28484 | 97 |
Time.+ (Time.now(), Time.fromSeconds 10) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
98 |
else |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
99 |
#1 (ThreadHeap.min (! timeout_heap)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
100 |
in |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
101 |
wait_for_next_event next_time |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
102 |
end |
28478 | 103 |
in wait_for_next_event Time.zeroTime end) |
104 |
in managing_thread := SOME new_thread end |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
105 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
106 |
(* calling thread registers itself to be managed here with a relative timeout *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
107 |
fun register birthtime deadtime (thread, name) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
108 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
109 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
110 |
(* create the atp-managing-thread if this is the first call to register *) |
28478 | 111 |
val _ = |
112 |
if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false) |
|
113 |
then () else start () |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
114 |
(* insertion *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
115 |
val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
116 |
val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
117 |
val _ = change active (cons (thread, birthtime, deadtime, name)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
118 |
(*maximum number of atps must not exceed*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
119 |
val _ = let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
120 |
fun kill_oldest () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
121 |
let val (_, oldest_thread) = ThreadHeap.min (!oldest_heap) |
28484 | 122 |
val _ = change oldest_heap ThreadHeap.delete_min |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
123 |
in unregister_locked oldest_thread end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
124 |
in |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
125 |
while ! maximum_atps > ~1 andalso length (! active) > ! maximum_atps |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
126 |
do kill_oldest () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
127 |
end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
128 |
(* state of threadmanager changed => signal *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
129 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
130 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
131 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
132 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
133 |
(* calling Thread unregisters itself from Threadmanager; thread is responsible |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
134 |
to terminate after calling this method *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
135 |
fun unregister success = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
136 |
let val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
137 |
val thread = Thread.self () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
138 |
(* get birthtime of unregistering thread - for group-killing*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
139 |
fun get_birthtime [] = Time.zeroTime |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
140 |
| get_birthtime ((t,tb,td,desc)::actives) = if Thread.equal (thread, t) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
141 |
then tb |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
142 |
else get_birthtime actives |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
143 |
val birthtime = get_birthtime (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
144 |
(* remove unregistering thread *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
145 |
val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
146 |
val _ = if (! groupkilling) andalso success |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
147 |
then (* remove all threads of the same group *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
148 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
149 |
val group_threads = filter (fn (_, tb, _, _) => tb = birthtime) (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
150 |
val _ = change cancelling (append group_threads) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
151 |
val _ = change active (filter_out (fn (_, tb, _, _) => tb = birthtime)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
152 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
153 |
else () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
154 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
155 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
156 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
157 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
158 |
(* Move all threads to cancelling *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
159 |
fun kill_all () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
160 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
161 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
162 |
val _ = change active (map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
163 |
val _ = change cancelling (append (! active)) |
28484 | 164 |
val _ = active := [] |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
165 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
166 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
167 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
168 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
169 |
fun info () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
170 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
171 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
172 |
fun running_info (_, birth_time, dead_time, desc) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
173 |
priority ("Running: " |
28484 | 174 |
^ ((Int.toString o Time.toSeconds) (Time.- (Time.now(), birth_time))) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
175 |
^ " s -- " |
28484 | 176 |
^ ((Int.toString o Time.toSeconds) (Time.- (dead_time, Time.now()))) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
177 |
^ " s to live:\n" ^ desc) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
178 |
fun cancelling_info (_, _, dead_time, desc) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
179 |
priority ("Trying to interrupt thread since " |
28484 | 180 |
^ (Int.toString o Time.toSeconds) (Time.- (Time.now(), dead_time)) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
181 |
^ " s:\n" ^ desc ) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
182 |
val _ = if length (! active) = 0 then [priority "No ATPs running."] |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
183 |
else (priority "--- RUNNING ATPs ---"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
184 |
map (fn entry => running_info entry) (! active)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
185 |
val _ = if length (! cancelling) = 0 then [] |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
186 |
else (priority "--- TRYING TO INTERRUPT FOLLOWING ATPs ---"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
187 |
map (fn entry => cancelling_info entry) (! cancelling)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
188 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
189 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
190 |
|
28484 | 191 |
|
192 |
(* preferences *) |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
193 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
194 |
fun set_max_atp number = CRITICAL (fn () => maximum_atps := number); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
195 |
fun set_atps str = CRITICAL (fn () => atps := str); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
196 |
fun set_timeout time = CRITICAL (fn () => timeout := time); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
197 |
fun set_groupkilling boolean = CRITICAL (fn () => groupkilling := boolean); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
198 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
199 |
val _ = ProofGeneralPgip.add_preference "Proof" |
28484 | 200 |
{name = "ATP - Provers (see print_atps)", |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
201 |
descr = "Which external automatic provers (seperated by commas)", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
202 |
default = !atps, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
203 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
204 |
get = fn () => !atps, |
28484 | 205 |
set = set_atps} |
28487
13e637e0c876
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
wenzelm
parents:
28484
diff
changeset
|
206 |
handle ERROR _ => warning "Preference already exists"; |
28484 | 207 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
208 |
val _ = ProofGeneralPgip.add_preference "Proof" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
209 |
{name = "ATP - Maximum number", |
28484 | 210 |
descr = "How many provers may run in parallel", |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
211 |
default = Int.toString (! maximum_atps), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
212 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
213 |
get = fn () => Int.toString (! maximum_atps), |
28484 | 214 |
set = fn str => set_max_atp (the_default 1 (Int.fromString str))} |
28487
13e637e0c876
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
wenzelm
parents:
28484
diff
changeset
|
215 |
handle ERROR _ => warning "Preference already exists"; |
28484 | 216 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
217 |
val _ = ProofGeneralPgip.add_preference "Proof" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
218 |
{name = "ATP - Timeout", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
219 |
descr = "ATPs will be interrupted after this time (in seconds)", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
220 |
default = Int.toString (! timeout), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
221 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
222 |
get = fn () => Int.toString (! timeout), |
28484 | 223 |
set = fn str => set_timeout (the_default 60 (Int.fromString str))} |
28487
13e637e0c876
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
wenzelm
parents:
28484
diff
changeset
|
224 |
handle ERROR _ => warning "Preference already exists"; |
28484 | 225 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
226 |
|
28484 | 227 |
(* named provers *) |
228 |
||
229 |
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name); |
|
230 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
231 |
structure Provers = TheoryDataFun |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
232 |
( |
28484 | 233 |
type T = ((Proof.state -> Thread.thread * string) * stamp) Symtab.table |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
234 |
val empty = Symtab.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
235 |
val copy = I |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
236 |
val extend = I |
28484 | 237 |
fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs |
238 |
handle Symtab.DUP dup => err_dup_prover dup; |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
239 |
); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
240 |
|
28484 | 241 |
fun add_prover name prover_fn = |
242 |
Provers.map (Symtab.update_new (name, (prover_fn, stamp ()))) |
|
243 |
handle Symtab.DUP dup => err_dup_prover dup; |
|
244 |
||
245 |
fun print_provers thy = Pretty.writeln |
|
246 |
(Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy)))); |
|
247 |
||
248 |
fun run_prover state name = |
|
249 |
(case Symtab.lookup (Provers.get (Proof.theory_of state)) name of |
|
250 |
NONE => (warning ("Unknown external prover: " ^ quote name); NONE) |
|
251 |
| SOME (prover_fn, _) => SOME (prover_fn state)); |
|
252 |
||
253 |
||
254 |
(* sledghammer *) |
|
255 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
256 |
fun sledgehammer state = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
257 |
let |
28484 | 258 |
val proverids = String.tokens (fn c => c = #",") (! atps) |
259 |
val threads_names = map_filter (run_prover state) proverids |
|
260 |
val birthtime = Time.now() |
|
261 |
val deadtime = Time.+ (Time.now(), Time.fromSeconds (! timeout)) |
|
262 |
val _ = List.app (register birthtime deadtime) threads_names |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
263 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
264 |
|
28484 | 265 |
|
266 |
(* concrete syntax *) |
|
267 |
||
268 |
local structure K = OuterKeyword and P = OuterParse in |
|
269 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
270 |
val _ = |
28484 | 271 |
OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag |
272 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_all)); |
|
273 |
||
274 |
val _ = |
|
275 |
OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag |
|
276 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)); |
|
277 |
||
278 |
val _ = |
|
279 |
OuterSyntax.improper_command "print_atps" "print external provers" K.diag |
|
280 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o |
|
281 |
Toplevel.keep (print_provers o Toplevel.theory_of))); |
|
282 |
||
283 |
val _ = |
|
284 |
OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag |
|
285 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o |
|
286 |
Toplevel.keep (sledgehammer o Toplevel.proof_of))); |
|
287 |
||
288 |
end; |
|
289 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
290 |
end; |