8 or when the maximum number of threads exceeds; then the oldest thread is killed. |
8 or when the maximum number of threads exceeds; then the oldest thread is killed. |
9 *) |
9 *) |
10 |
10 |
11 signature ATP_MANAGER = |
11 signature ATP_MANAGER = |
12 sig |
12 sig |
13 val get_atps: unit -> string |
13 val atps: string Unsynchronized.ref |
14 val set_atps: string -> unit |
14 val get_atps: unit -> string list |
15 val get_max_atps: unit -> int |
15 val max_atps: int Unsynchronized.ref |
16 val set_max_atps: int -> unit |
16 val timeout: int Unsynchronized.ref |
17 val get_timeout: unit -> int |
17 val full_types: bool Unsynchronized.ref |
18 val set_timeout: int -> unit |
|
19 val get_full_types: unit -> bool |
|
20 val set_full_types: bool -> unit |
|
21 val kill: unit -> unit |
18 val kill: unit -> unit |
22 val info: unit -> unit |
19 val info: unit -> unit |
23 val messages: int option -> unit |
20 val messages: int option -> unit |
24 val add_prover: string * ATP_Wrapper.prover -> theory -> theory |
21 val add_prover: string * ATP_Wrapper.prover -> theory -> theory |
25 val print_provers: theory -> unit |
22 val print_provers: theory -> unit |
33 (** preferences **) |
30 (** preferences **) |
34 |
31 |
35 val message_store_limit = 20; |
32 val message_store_limit = 20; |
36 val message_display_limit = 5; |
33 val message_display_limit = 5; |
37 |
34 |
38 local |
|
39 |
|
40 val atps = Unsynchronized.ref "e spass remote_vampire"; |
35 val atps = Unsynchronized.ref "e spass remote_vampire"; |
|
36 fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps); |
|
37 |
41 val max_atps = Unsynchronized.ref 5; (* ~1 means infinite number of atps *) |
38 val max_atps = Unsynchronized.ref 5; (* ~1 means infinite number of atps *) |
42 val timeout = Unsynchronized.ref 60; |
39 val timeout = Unsynchronized.ref 60; |
43 val full_types = Unsynchronized.ref false; |
40 val full_types = Unsynchronized.ref false; |
44 |
41 |
45 in |
|
46 |
|
47 fun get_atps () = CRITICAL (fn () => ! atps); |
|
48 fun set_atps str = CRITICAL (fn () => atps := str); |
|
49 |
|
50 fun get_max_atps () = CRITICAL (fn () => ! max_atps); |
|
51 fun set_max_atps number = CRITICAL (fn () => max_atps := number); |
|
52 |
|
53 fun get_timeout () = CRITICAL (fn () => ! timeout); |
|
54 fun set_timeout time = CRITICAL (fn () => timeout := time); |
|
55 |
|
56 fun get_full_types () = CRITICAL (fn () => ! full_types); |
|
57 fun set_full_types bool = CRITICAL (fn () => full_types := bool); |
|
58 |
|
59 val _ = |
42 val _ = |
60 ProofGeneralPgip.add_preference Preferences.category_proof |
43 ProofGeneralPgip.add_preference Preferences.category_proof |
61 (Preferences.string_pref atps |
44 (Preferences.string_pref atps |
62 "ATP: provers" "Default automatic provers (separated by whitespace)"); |
45 "ATP: provers" "Default automatic provers (separated by whitespace)"); |
63 |
46 |
335 "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ |
316 "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ |
336 Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)) |
317 Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)) |
337 val _ = SimpleThread.fork true (fn () => |
318 val _ = SimpleThread.fork true (fn () => |
338 let |
319 let |
339 val _ = register birthtime deadtime (Thread.self (), desc) |
320 val _ = register birthtime deadtime (Thread.self (), desc) |
340 val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i |
321 val problem = |
341 (Proof.get_goal proof_state) |
322 ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state) |
342 val result = |
323 val result = |
343 let val ATP_Wrapper.Prover_Result {success, message, ...} = |
324 let val ATP_Wrapper.Prover_Result {success, message, ...} = |
344 prover problem (get_timeout ()) |
325 prover problem (! timeout) |
345 in (success, message) end |
326 in (success, message) end |
346 handle ResHolClause.TOO_TRIVIAL |
327 handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *) |
347 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis") |
328 (true, "Empty clause: Try this command: " ^ |
348 | ERROR msg |
329 Markup.markup Markup.sendback "apply metis") |
349 => (false, "Error: " ^ msg) |
330 | ERROR msg => (false, "Error: " ^ msg) |
350 val _ = unregister result (Thread.self ()) |
331 val _ = unregister result (Thread.self ()) |
351 in () end handle Interrupt => ()) |
332 in () end handle Interrupt => ()) |
352 in () end); |
333 in () end); |
353 |
334 |
354 |
335 |
355 (* sledghammer for first subgoal *) |
336 (* sledghammer for first subgoal *) |
356 |
337 |
357 fun sledgehammer names proof_state = |
338 fun sledgehammer names proof_state = |
358 let |
339 let |
359 val provers = |
340 val provers = if null names then get_atps () else names |
360 if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ()) |
|
361 else names |
|
362 val birthtime = Time.now () |
341 val birthtime = Time.now () |
363 val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ())) |
342 val deadtime = Time.+ (birthtime, Time.fromSeconds (! timeout)) |
364 in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end; |
343 in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end; |
365 |
344 |
366 |
345 |
367 |
346 |
368 (** Isar command syntax **) |
347 (** Isar command syntax **) |