src/HOL/Tools/atp_manager.ML
author wenzelm
Mon, 13 Oct 2008 14:04:28 +0200
changeset 28571 47d88239658d
parent 28543 637f2808ab64
child 28582 c269a3045fdf
permissions -rw-r--r--
** Update from Fabian ** preferences/provers: separated by white space, avoid low-level char type; sledgehammer command accepts prover list as well; avoid I/O in critical section of AtpManager.info; more systematic synchronization using higher-order combinators; more descriptive errors when atp fails; keep explicitly requested problem files; added remote prover functions; simplified treatment of prover name in diagnostic output; misc tuning and cleanup;
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
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     5
ATP threads are registered here.
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     6
Threads with the same birth-time are seen as one group.
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     7
All threads of a group are killed when one thread of it has been successful,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     8
or after a certain time,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     9
or when the maximum number of threads exceeds; then the oldest thread is killed.
28477
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
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    15
  val info: unit -> string
28477
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
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    19
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    20
  val atp_thread: (unit -> 'a option) -> ('a -> string) -> Thread.thread
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    21
  val add_prover: string -> (int -> Proof.state -> Thread.thread) -> theory -> theory
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    22
  val print_provers: theory -> unit
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    23
  val sledgehammer: string list -> Proof.state -> unit
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    24
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    25
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    26
structure AtpManager : ATP_MANAGER =
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    27
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    28
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    29
  structure ThreadHeap = HeapFun
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    30
  (
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    31
    type elem = Time.time * Thread.thread;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    32
    fun ord ((a, _), (b, _)) = Time.compare (a, b);
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    33
  )
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    34
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    35
  (* state of threadmanager *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    36
  datatype T = State of {
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    37
      timeout_heap: ThreadHeap.T,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    38
      oldest_heap: ThreadHeap.T,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    39
      (* managed threads *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    40
      active: (Thread.thread * (Time.time * Time.time * string)) list,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    41
      cancelling: (Thread.thread * (Time.time * Time.time * string)) list
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    42
  }
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    43
  val state = ref (State {
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    44
        timeout_heap = ThreadHeap.empty,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    45
        oldest_heap = ThreadHeap.empty,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    46
        active = [],
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    47
        cancelling = []})
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    48
      
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    49
  (* synchronizing *)
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    50
  val lock = Mutex.mutex ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    51
  val state_change = ConditionVar.conditionVar ()
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    52
  (* watches over running threads and interrupts them if required *)
28478
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
    53
  val managing_thread = ref (NONE: Thread.thread option);
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    54
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    55
  (* active and cancelling are association lists *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    56
  val lookup_th = AList.lookup Thread.equal;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    57
  val delete_th = AList.delete Thread.equal;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    58
  val update_th = AList.update Thread.equal;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    59
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    60
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    61
  (* waiting for a condition, checking it after time or when signalled
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    62
     then changing state with returning a result *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    63
  fun protected_wait_change_result P time f = uninterruptible (fn restore => fn () =>
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    64
      let
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    65
      val _ = Mutex.lock lock;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    66
      val _ = while not (P (! state)) do ConditionVar.waitUntil (state_change, lock, time (! state));
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    67
      val res = Exn.Result (restore (fn () => change_result state f) ()) handle exn => Exn.Exn exn
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    68
      val _ = ConditionVar.broadcast state_change;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    69
      val _ = Mutex.unlock lock;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    70
  in Exn.release res end) ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    71
  
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    72
  fun protected_change f = protected_wait_change_result (fn _ => true) (fn _ => Time.zeroTime) f;
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    73
  
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    74
  fun protected f = protected_change (`f);
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    75
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    76
  (* unregister Thread from Threadmanager = move to cancelling *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    77
  fun unregister success message thread = protected_change (fn State {timeout_heap, oldest_heap, active, cancelling} => 
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    78
    let
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    79
    val info = lookup_th active thread
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    80
    (* get birthtime of unregistering thread if successful - for group-killing*)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    81
    val birthtime = case info of NONE => Time.zeroTime
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    82
      | SOME (tb, _, _) => if success then tb else Time.zeroTime
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    83
    (* move unregistering thread to cancelling *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    84
    val active' = delete_th thread active
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    85
    val cancelling' = case info of NONE => cancelling
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    86
      | SOME (tb, _, desc) => update_th (thread, (tb, Time.now(), desc)) cancelling
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    87
    (* move all threads of the same group to cancelling *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    88
    val group_threads = map_filter (fn (th, (tb, _, desc)) =>
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    89
        if tb = birthtime then SOME (th, (tb, Time.now(), desc)) else NONE)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    90
      active 
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    91
    val active'' = filter_out (fn (_, (tb, _, _)) => tb = birthtime) active'
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    92
    val cancelling'' = append group_threads cancelling'
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    93
    (* message for user *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    94
    val message = case info of NONE => ""
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    95
      | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n    " ^ message ^
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    96
        (if length group_threads > 1
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    97
        then "\n\nInterrupted " ^ Int.toString (length group_threads - 1) ^ " others of group."
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    98
        else "")
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    99
    in (message, State {timeout_heap = timeout_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   100
                  oldest_heap = oldest_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   101
                  active = active'',
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   102
                  cancelling = cancelling''})
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   103
    end)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   104
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   105
  (* start a watching thread which runs forever - only one may exist => checked by register *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   106
  fun start () = managing_thread := SOME (SimpleThread.fork false (fn () =>
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   107
    let
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   108
    val min_wait_time = Time.fromMilliseconds 300
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   109
    val max_wait_time = Time.fromSeconds 10
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   110
    (* action is required when there are cancelling threads, or a thread is to be cancelled *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   111
    fun P (State {timeout_heap, oldest_heap, active, cancelling}) =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   112
      length cancelling > 0  orelse
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   113
        (not (ThreadHeap.is_empty timeout_heap) andalso
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   114
        Time.< (#1 (ThreadHeap.min timeout_heap), Time.now ()))
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   115
    (* wait for next thread to cancel, or a maximum of 10 Seconds*)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   116
    fun time (State {timeout_heap, oldest_heap, active, cancelling}) =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   117
      if ThreadHeap.is_empty timeout_heap then Time.+ (Time.now(), max_wait_time)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   118
      else #1 (ThreadHeap.min timeout_heap)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   119
    (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   120
    fun action (State {timeout_heap, oldest_heap, active, cancelling}) =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   121
      let
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   122
      (* find out threads wich reached their timeout *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   123
      fun find_threads (heap, threads) =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   124
        if ThreadHeap.is_empty heap then (heap, threads) else
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   125
          let val (mintime, minthread) = ThreadHeap.min heap
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   126
          in if Time.> (mintime, Time.now())
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   127
            then (heap, threads)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   128
            else find_threads (ThreadHeap.delete_min heap, minthread :: threads)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   129
          end
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   130
      val (timeout_heap', timeout_threads) = find_threads (timeout_heap, [])
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   131
      val _ = List.app (SimpleThread.interrupt o fst) cancelling
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   132
      val cancelling' = filter (fn (t, _) => Thread.isActive t) cancelling
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   133
      (* return threads with timeout and changed state *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   134
      in (timeout_threads, State {timeout_heap = timeout_heap',
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   135
                    oldest_heap = oldest_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   136
                    active = active,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   137
                    cancelling = cancelling'})
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   138
      end
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   139
    in while true do 
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   140
        (* cancel threads found by 'action' *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   141
        (map (priority o (unregister false "Interrupted (reached timeout)")) (protected_wait_change_result P time action);
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   142
        (* give threads time to respond to interrupt *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   143
        OS.Process.sleep min_wait_time)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   144
    end))
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   145
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   146
  (* calling thread is registered here by sledgehammer *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   147
  fun register birthtime deadtime (thread, desc) = protected_change (
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   148
    fn State {timeout_heap, oldest_heap, active, cancelling} => 
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   149
    let val _ = (* 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
   150
      if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
855ca2dcc03d simplified thread creation via SimpleThread;
wenzelm
parents: 28477
diff changeset
   151
      then () else start ()
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   152
    (* insertion *)
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   153
    in ((),State {timeout_heap = ThreadHeap.insert (deadtime, thread) timeout_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   154
                  oldest_heap = ThreadHeap.insert (birthtime, thread) oldest_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   155
                  active = update_th (thread, (birthtime, deadtime, desc)) active,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   156
                  cancelling = cancelling})
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   157
    end)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   158
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   159
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   160
  (* Move all threads to cancelling *)
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   161
  fun kill_all () = protected_change (fn State {timeout_heap, oldest_heap, active, cancelling} =>
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   162
    let
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   163
    val active' = (map (fn (th, (tb, _, desc)) => (th, (tb, Time.now(), desc))) active)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   164
    in ((),State {timeout_heap = timeout_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   165
                  oldest_heap = oldest_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   166
                  active = [],
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   167
                  cancelling = append active' cancelling})
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   168
    end)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   169
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   170
  (* give information on running threads *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   171
  fun info () = protected (fn State {timeout_heap, oldest_heap, active, cancelling} =>
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   172
    let
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   173
    fun running_info (_, (birth_time, dead_time, desc)) = "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())))
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   177
        ^ " s to live:\n" ^ desc
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   178
    fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   179
        ^ (Int.toString o Time.toSeconds) (Time.- (Time.now(), dead_time))
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   180
        ^ " s:\n" ^ desc
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   181
    val running = if null active then "No ATPs running."
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   182
      else String.concatWith "\n\n" ("--- RUNNING ATPs ---" ::
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   183
      (map (fn entry => running_info entry) active))
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   184
    val interrupting = if null cancelling then ""
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   185
      else String.concatWith "\n\n" ("--- TRYING TO INTERRUPT FOLLOWING ATPs ---" ::
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   186
      (map (fn entry => cancelling_info entry) cancelling))
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   187
    in running ^ "\n" ^ interrupting end)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   188
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   189
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   190
    (* thread wrapping an atp-call *)   
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   191
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   192
    fun atp_thread call_prover produce_answer =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   193
      SimpleThread.fork true (fn () =>
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   194
        let
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   195
        val result = call_prover ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   196
        val message = case result of NONE => "Failed."
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   197
            | SOME result => "Try this command: " ^ produce_answer result
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   198
        in priority (unregister (isSome result) message (Thread.self()))
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   199
        end handle Interrupt => ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   200
      )
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   201
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   202
      
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   203
    (* preferences *)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   204
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   205
    val atps = ref "e spass"
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   206
    val maximum_atps = ref 5   (* ~1 means infinite number of atps*)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   207
    val timeout = ref 60
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   208
    val groupkilling = ref true
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   209
    fun set_atps str = CRITICAL (fn () => atps := str);
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   210
    fun set_max_atp number = CRITICAL (fn () => maximum_atps := number);
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   211
    fun set_timeout time = CRITICAL (fn () => timeout := time);
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   212
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   213
    val _ = ProofGeneralPgip.add_preference "Proof"
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   214
        {name = "ATP - Provers (see print_atps)",
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   215
         descr = "Default automatic provers (seperated by whitespace)",
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   216
         default = !atps,
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   217
         pgiptype = PgipTypes.Pgipstring,
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   218
         get = fn () => !atps,
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   219
         set = set_atps}
28487
13e637e0c876 do not handle Error (which matches arbitrary exceptions!), but ERROR _;
wenzelm
parents: 28484
diff changeset
   220
        handle ERROR _ => warning "Preference already exists";
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   221
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   222
    val _ = ProofGeneralPgip.add_preference "Proof"
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   223
        {name = "ATP - Maximum number",
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   224
         descr = "How many provers may run in parallel",
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   225
         default = Int.toString (! maximum_atps),
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   226
         pgiptype = PgipTypes.Pgipstring,
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   227
         get = fn () => Int.toString (! maximum_atps),
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   228
         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
   229
        handle ERROR _ => warning "Preference already exists";
28484
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
    val _ = ProofGeneralPgip.add_preference "Proof"
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   232
        {name = "ATP - Timeout",
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   233
         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
   234
         default = Int.toString (! timeout),
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   235
         pgiptype = PgipTypes.Pgipstring,
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   236
         get = fn () => Int.toString (! timeout),
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   237
         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
   238
        handle ERROR _ => warning "Preference already exists";
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   239
28477
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
  (* named provers *)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   242
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   243
  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   244
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   245
  structure Provers = TheoryDataFun
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   246
  (
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   247
    type T = ((int -> Proof.state -> Thread.thread) * stamp) Symtab.table
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   248
    val empty = Symtab.empty
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   249
    val copy = I
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   250
    val extend = I
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   251
    fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   252
      handle Symtab.DUP dup => err_dup_prover dup;
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   253
  );
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   254
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   255
  fun add_prover name prover_fn =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   256
    Provers.map (Symtab.update_new (name, (prover_fn, stamp ())))
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   257
      handle Symtab.DUP dup => err_dup_prover dup;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   258
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   259
  fun print_provers thy = Pretty.writeln
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   260
    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   261
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   262
  fun prover_desc state subgoal name =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   263
     let val (ctxt, (chain_ths, goal)) = Proof.get_goal state
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   264
     in "External prover " ^ quote name ^ " for Subgoal " ^ Int.toString subgoal^ ":\n" ^ Syntax.string_of_term ctxt (List.nth(prems_of goal, subgoal-1)) end   
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   265
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   266
  fun run_prover state subgoal name =
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   267
    (case Symtab.lookup (Provers.get (Proof.theory_of state)) name of
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   268
      NONE => (warning ("Unknown external prover: " ^ quote name); NONE)
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   269
    | SOME (prover_fn, _) => SOME (prover_fn subgoal state, prover_desc state subgoal name));
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   270
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   271
  fun kill_one () = 
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   272
    let
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   273
    val oldest = protected_change (fn (s as State {timeout_heap , oldest_heap, active, cancelling}) =>
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   274
      if ThreadHeap.is_empty oldest_heap orelse length active <= !maximum_atps orelse ! maximum_atps = ~1 then (NONE, s)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   275
      else
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   276
      let val (_, oldest_thread) = ThreadHeap.min (oldest_heap)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   277
      in (SOME oldest_thread, State {timeout_heap = timeout_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   278
        oldest_heap = ThreadHeap.delete_min oldest_heap,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   279
        active = active,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   280
        cancelling = cancelling}) end)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   281
    in case oldest of NONE => ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   282
      | SOME thread => priority (unregister false "Interrupted (Maximum number of ATPs exceeded)." thread) end
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   283
      
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   284
  fun kill_oldest (State {timeout_heap, oldest_heap, active, cancelling}) =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   285
    if length active > !maximum_atps andalso !maximum_atps > ~1
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   286
    then let val _ = kill_one () in kill_oldest (! state) end
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   287
    else ()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   288
      
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   289
    
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   290
  (* sledghammer for first subgoal *)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   291
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   292
  fun sledgehammer names proof_state =
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   293
    let
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   294
    val proverids = case names of
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   295
      [] => String.tokens (Symbol.is_ascii_blank o String.str) (! atps)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   296
      | names => names
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   297
    val threads_names = map_filter (run_prover proof_state 1) proverids
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   298
    val birthtime = Time.now()
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   299
    val deadtime = Time.+ (Time.now(), Time.fromSeconds (! timeout))
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   300
    val _ = List.app (register birthtime deadtime) threads_names
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   301
      (*maximum number of atps must not exceed*)
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   302
    val _ = kill_oldest (! state)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   303
    in () end
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   304
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   305
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   306
  (* concrete syntax *)
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   307
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   308
  local structure K = OuterKeyword and P = OuterParse in
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   309
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   310
  val _ =
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   311
    OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   312
      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_all));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   313
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   314
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   315
    OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   316
      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (priority o info)));
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   317
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   318
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   319
    OuterSyntax.improper_command "print_atps" "print external provers" K.diag
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   320
      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   321
        Toplevel.keep (print_provers o Toplevel.theory_of)));
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   322
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   323
  val _ =
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   324
    OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   325
      (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   326
      Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   327
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   328
  end;
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   329
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   330
end;