src/HOL/Tools/ATP_Manager/atp_manager.ML
author wenzelm
Thu Oct 15 17:06:19 2009 +0200 (2009-10-15)
changeset 32947 3c19b98a35cd
parent 32941 72d48e333b77
child 32948 e95a4be101a8
permissions -rw-r--r--
ATP_Manager.get_prover: canonical argument order;
eliminated various aliases of existing operations, notably Output channels;
tuned messages;
misc tuning and clarification;
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
     2     Author:     Fabian Immler, TU Muenchen
     3 
     4 ATP threads are registered here.
     5 Threads with the same birth-time are seen as one group.
     6 All threads of a group are killed when one thread of it has been successful,
     7 or after a certain time,
     8 or when the maximum number of threads exceeds; then the oldest thread is killed.
     9 *)
    10 
    11 signature ATP_MANAGER =
    12 sig
    13   val atps: string Unsynchronized.ref
    14   val get_atps: unit -> string list
    15   val max_atps: int Unsynchronized.ref
    16   val timeout: int Unsynchronized.ref
    17   val full_types: bool Unsynchronized.ref
    18   val kill: unit -> unit
    19   val info: unit -> unit
    20   val messages: int option -> unit
    21   val add_prover: string * ATP_Wrapper.prover -> theory -> theory
    22   val print_provers: theory -> unit
    23   val get_prover: theory -> string -> ATP_Wrapper.prover option
    24   val sledgehammer: string list -> Proof.state -> unit
    25 end;
    26 
    27 structure ATP_Manager: ATP_MANAGER =
    28 struct
    29 
    30 (** preferences **)
    31 
    32 val message_store_limit = 20;
    33 val message_display_limit = 5;
    34 
    35 val atps = Unsynchronized.ref "e spass remote_vampire";
    36 fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
    37 
    38 val max_atps = Unsynchronized.ref 5;
    39 fun excessive_atps active =
    40   let val max = ! max_atps
    41   in max >= 0 andalso length active > max end;
    42 
    43 val timeout = Unsynchronized.ref 60;
    44 val full_types = Unsynchronized.ref false;
    45 
    46 val _ =
    47   ProofGeneralPgip.add_preference Preferences.category_proof
    48     (Preferences.string_pref atps
    49       "ATP: provers" "Default automatic provers (separated by whitespace)");
    50 
    51 val _ =
    52   ProofGeneralPgip.add_preference Preferences.category_proof
    53     (Preferences.int_pref max_atps
    54       "ATP: maximum number" "How many provers may run in parallel");
    55 
    56 val _ =
    57   ProofGeneralPgip.add_preference Preferences.category_proof
    58     (Preferences.int_pref timeout
    59       "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
    60 
    61 val _ =
    62   ProofGeneralPgip.add_preference Preferences.category_proof
    63     (Preferences.bool_pref full_types
    64       "ATP: full types" "ATPs will use full type information");
    65 
    66 
    67 
    68 (** thread management **)
    69 
    70 (* data structures over threads *)
    71 
    72 structure Thread_Heap = Heap
    73 (
    74   type elem = Time.time * Thread.thread;
    75   fun ord ((a, _), (b, _)) = Time.compare (a, b);
    76 );
    77 
    78 fun lookup_thread xs = AList.lookup Thread.equal xs;
    79 fun update_thread xs = AList.update Thread.equal xs;
    80 
    81 
    82 (* state of thread manager *)
    83 
    84 type state =
    85  {manager: Thread.thread option,
    86   timeout_heap: Thread_Heap.T,
    87   oldest_heap: Thread_Heap.T,
    88   active: (Thread.thread * (Time.time * Time.time * string)) list,
    89   cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
    90   messages: string list,
    91   store: string list};
    92 
    93 fun make_state manager timeout_heap oldest_heap active cancelling messages store =
    94   {manager = manager, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
    95     active = active, cancelling = cancelling, messages = messages, store = store};
    96 
    97 val global_state = Synchronized.var "atp_manager"
    98   (make_state NONE Thread_Heap.empty Thread_Heap.empty [] [] [] []);
    99 
   100 
   101 (* unregister thread *)
   102 
   103 fun unregister (success, message) thread = Synchronized.change global_state
   104   (fn state as {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   105     (case lookup_thread active thread of
   106       SOME (birthtime, _, description) =>
   107         let
   108           val (group, active') =
   109             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
   110             else List.partition (fn (th, _) => Thread.equal (th, thread)) active;
   111 
   112           val now = Time.now ();
   113           val cancelling' =
   114             fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling;
   115 
   116           val message' = description ^ "\n" ^ message ^
   117             (if length group <= 1 then ""
   118              else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members");
   119           val store' = message' ::
   120             (if length store <= message_store_limit then store
   121              else #1 (chop message_store_limit store));
   122         in
   123           make_state manager timeout_heap oldest_heap
   124             active' cancelling' (message' :: messages) store'
   125         end
   126     | NONE => state));
   127 
   128 
   129 (* kill excessive atp threads *)
   130 
   131 local
   132 
   133 exception UNCHANGED of unit;
   134 
   135 fun kill_oldest () =
   136   Synchronized.change_result global_state
   137     (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   138       if Thread_Heap.is_empty oldest_heap orelse not (excessive_atps active)
   139       then raise UNCHANGED ()
   140       else
   141         let
   142           val ((_, oldest_thread), oldest_heap') = Thread_Heap.min_elem oldest_heap;
   143           val state' =
   144             make_state manager timeout_heap oldest_heap' active cancelling messages store;
   145         in (oldest_thread, state') end)
   146     |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
   147   handle UNCHANGED () => ();
   148 
   149 in
   150 
   151 fun kill_excessive () =
   152   let val {active, ...} = Synchronized.value global_state
   153   in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
   154 
   155 end;
   156 
   157 fun print_new_messages () =
   158   let val msgs = Synchronized.change_result global_state
   159     (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   160       (messages, make_state manager timeout_heap oldest_heap active cancelling [] store))
   161   in
   162     if null msgs then ()
   163     else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
   164   end;
   165 
   166 
   167 (* start manager thread -- only one may exist *)
   168 
   169 val min_wait_time = Time.fromMilliseconds 300;
   170 val max_wait_time = Time.fromSeconds 10;
   171 
   172 fun check_thread_manager () = Synchronized.change global_state
   173   (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   174     if (case manager of SOME thread => Thread.isActive thread | NONE => false)
   175     then make_state manager timeout_heap oldest_heap active cancelling messages store
   176     else let val manager = SOME (SimpleThread.fork false (fn () =>
   177       let
   178         fun time_limit timeout_heap =
   179           (case try Thread_Heap.min timeout_heap of
   180             NONE => Time.+ (Time.now (), max_wait_time)
   181           | SOME (time, _) => time);
   182 
   183         (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
   184         fun action {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =
   185           let val (timeout_threads, timeout_heap') =
   186             Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   187           in
   188             if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
   189             then NONE
   190             else
   191               let
   192                 val _ = List.app (SimpleThread.interrupt o #1) cancelling;
   193                 val cancelling' = filter (Thread.isActive o #1) cancelling;
   194                 val state' =
   195                   make_state manager timeout_heap' oldest_heap active cancelling' messages store;
   196               in SOME (map #2 timeout_threads, state') end
   197           end;
   198       in
   199         while Synchronized.change_result global_state
   200           (fn state as {timeout_heap, oldest_heap, active, cancelling, messages, store, ...} =>
   201             if null active andalso null cancelling andalso null messages
   202             then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
   203             else (true, state))
   204         do
   205           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   206             |> these
   207             |> List.app (unregister (false, "Interrupted (reached timeout)"));
   208             kill_excessive ();
   209             print_new_messages ();
   210             (*give threads some time to respond to interrupt*)
   211             OS.Process.sleep min_wait_time)
   212       end))
   213     in make_state manager timeout_heap oldest_heap active cancelling messages store end);
   214 
   215 
   216 (* thread is registered here by sledgehammer *)
   217 
   218 fun register birthtime deadtime (thread, desc) =
   219  (Synchronized.change global_state
   220     (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   221       let
   222         val timeout_heap' = Thread_Heap.insert (deadtime, thread) timeout_heap;
   223         val oldest_heap' = Thread_Heap.insert (birthtime, thread) oldest_heap;
   224         val active' = update_thread (thread, (birthtime, deadtime, desc)) active;
   225         val state' =
   226           make_state manager timeout_heap' oldest_heap' active' cancelling messages store;
   227       in state' end);
   228   check_thread_manager ());
   229 
   230 
   231 
   232 (** user commands **)
   233 
   234 (* kill: move all threads to cancelling *)
   235 
   236 fun kill () = Synchronized.change global_state
   237   (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   238     let
   239       val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active;
   240       val state' =
   241         make_state manager timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store;
   242     in state' end);
   243 
   244 
   245 (* ATP info *)
   246 
   247 fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
   248 
   249 fun info () =
   250   let
   251     val {active, cancelling, ...} = Synchronized.value global_state;
   252 
   253     val now = Time.now ();
   254     fun running_info (_, (birth_time, dead_time, desc)) =
   255       "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   256         seconds (Time.- (dead_time, now)) ^ " to live:\n" ^ desc;
   257     fun cancelling_info (_, (_, dead_time, desc)) =
   258       "Trying to interrupt thread since " ^ seconds (Time.- (now, dead_time)) ^ ":\n" ^ desc;
   259 
   260     val running =
   261       if null active then "No ATPs running."
   262       else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
   263     val interrupting =
   264       if null cancelling then ""
   265       else
   266         space_implode "\n\n"
   267           ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
   268 
   269   in writeln (running ^ "\n" ^ interrupting) end;
   270 
   271 fun messages opt_limit =
   272   let
   273     val limit = the_default message_display_limit opt_limit;
   274     val {store, ...} = Synchronized.value global_state;
   275     val header =
   276       "Recent ATP messages" ^
   277         (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
   278   in writeln (space_implode "\n\n" (header :: #1 (chop limit store))) end;
   279 
   280 
   281 
   282 (** The Sledgehammer **)
   283 
   284 (* named provers *)
   285 
   286 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
   287 
   288 structure Provers = TheoryDataFun
   289 (
   290   type T = (ATP_Wrapper.prover * stamp) Symtab.table;
   291   val empty = Symtab.empty;
   292   val copy = I;
   293   val extend = I;
   294   fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
   295     handle Symtab.DUP dup => err_dup_prover dup;
   296 );
   297 
   298 fun add_prover (name, prover) thy =
   299   Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
   300     handle Symtab.DUP dup => err_dup_prover dup;
   301 
   302 fun print_provers thy = Pretty.writeln
   303   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
   304 
   305 fun get_prover thy name =
   306   (case Symtab.lookup (Provers.get thy) name of
   307     NONE => NONE
   308   | SOME (prover, _) => SOME prover);
   309 
   310 
   311 (* start prover thread *)
   312 
   313 fun start_prover name birthtime deadtime i proof_state =
   314   (case get_prover (Proof.theory_of proof_state) name of
   315     NONE => warning ("Unknown external prover: " ^ quote name)
   316   | SOME prover =>
   317       let
   318         val (ctxt, (_, goal)) = Proof.get_goal proof_state;
   319         val desc =
   320           "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
   321             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
   322         val _ = SimpleThread.fork true (fn () =>
   323           let
   324             val _ = register birthtime deadtime (Thread.self (), desc);
   325             val problem =
   326               ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state);
   327             val result =
   328               let val {success, message, ...} = prover problem (! timeout);
   329               in (success, message) end
   330               handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
   331                   (true, "Empty clause: Try this command: " ^
   332                     Markup.markup Markup.sendback "apply metis")
   333                 | ERROR msg => (false, "Error: " ^ msg);
   334             val _ = unregister result (Thread.self ());
   335           in () end handle Exn.Interrupt => ())
   336       in () end);
   337 
   338 
   339 (* sledghammer for first subgoal *)
   340 
   341 fun sledgehammer names proof_state =
   342   let
   343     val provers = if null names then get_atps () else names;
   344     val birthtime = Time.now ();
   345     val deadtime = Time.+ (birthtime, Time.fromSeconds (! timeout));
   346   in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
   347 
   348 
   349 
   350 (** Isar command syntax **)
   351 
   352 local structure K = OuterKeyword and P = OuterParse in
   353 
   354 val _ =
   355   OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   356     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   357 
   358 val _ =
   359   OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
   360     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
   361 
   362 val _ =
   363   OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
   364     (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   365       (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
   366 
   367 val _ =
   368   OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   369     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   370       Toplevel.keep (print_provers o Toplevel.theory_of)));
   371 
   372 val _ =
   373   OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
   374     (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
   375       Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
   376 
   377 end;
   378 
   379 end;
   380