src/HOL/Tools/atp_manager.ML
author wenzelm
Fri, 03 Oct 2008 19:35:17 +0200
changeset 28484 4ed9239b09c1
parent 28478 855ca2dcc03d
child 28487 13e637e0c876
permissions -rw-r--r--
misc simplifcation and tuning; no export of structure Provers; added add_provers, print_provers; operate on Proof.state, not Toplevel.state; use Time.+ etc. to make SML/XL of NJ happy; explicit Isar commands 'atp_kill', 'atp_info', 'print_atps';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    23
  val add_prover: string -> (Proof.state -> Thread.thread * string) -> theory -> theory
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    24
  val print_provers: theory -> unit
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    31
  structure ThreadHeap = HeapFun
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    32
  (
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    33
    type elem = Time.time * Thread.thread;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    34
    fun ord ((a, _), (b, _)) = Time.compare (a, b);
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
    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
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
    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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    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
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   103
        in wait_for_next_event Time.zeroTime end)
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   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
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   111
    val _ =
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   112
      if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   191
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   205
         set = set_atps}
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   206
        handle Error => warning "Preference already exists";
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   214
         set = fn str => set_max_atp (the_default 1 (Int.fromString str))}
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   215
        handle Error => warning "Preference already exists";
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   223
         set = fn str => set_timeout (the_default 60 (Int.fromString str))}
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   224
        handle Error => warning "Preference already exists";
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   225
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   226
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   227
  (* named provers *)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   228
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   229
  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   237
    fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   241
  fun add_prover name prover_fn =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   242
    Provers.map (Symtab.update_new (name, (prover_fn, stamp ())))
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   243
      handle Symtab.DUP dup => err_dup_prover dup;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   244
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   245
  fun print_provers thy = Pretty.writeln
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   246
    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   247
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   248
  fun run_prover state name =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   249
    (case Symtab.lookup (Provers.get (Proof.theory_of state)) name of
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   250
      NONE => (warning ("Unknown external prover: " ^ quote name); NONE)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   251
    | SOME (prover_fn, _) => SOME (prover_fn state));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   252
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   253
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   254
  (* sledghammer *)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   258
      val proverids = String.tokens (fn c => c = #",") (! atps)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   259
      val threads_names = map_filter (run_prover state) proverids
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   260
      val birthtime = Time.now()
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   261
      val deadtime = Time.+ (Time.now(), Time.fromSeconds (! timeout))
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   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
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   265
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   266
  (* concrete syntax *)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   267
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   268
  local structure K = OuterKeyword and P = OuterParse in
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   269
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   270
  val _ =
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   271
    OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   272
      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_all));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   273
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   274
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   275
    OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   276
      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   277
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   278
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   279
    OuterSyntax.improper_command "print_atps" "print external provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   280
      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   281
        Toplevel.keep (print_provers o Toplevel.theory_of)));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   282
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   283
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   284
    OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   285
      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   286
        Toplevel.keep (sledgehammer o Toplevel.proof_of)));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   287
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   288
  end;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   289
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   290
end;