bench.ml 4.75 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
open Thread
open Why
open Env
open Theory
open Task
open Trans
open Driver
open Call_provers
open Scheduler

type 'a tool = {
  tval     : 'a;
  ttrans   : task trans;
  tdriver  : driver;
  tcommand : string;
  tenv     : env;
  tuse     : task;
  ttime    : int;
  tmem     : int;
}

type 'a prob = {
  ptask  : env -> task -> ('a * task) list; (** needed for tenv *)
  ptrans : task list trans;
}

type ('a,'b) result = {tool   : 'a;
                       prob   : 'b;
                       task   : task;
                       idtask : int;
                       result : prover_result}

type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit

let debug = Debug.register_flag "call"

module MTask :
sig
  type shared
  val create : unit -> shared
  val start : shared -> unit
  val stop : shared -> unit
  val lock : shared -> unit
  val unlock : shared -> unit
  val wait : shared -> unit
end
=
struct
  type shared =
      { m : Mutex.t; c : Condition.t;
        mutable nb_task : int;
      }

  let create () =
    { m = Mutex.create ();
      c = Condition.create ();
      nb_task = 0}

  let start s = Mutex.lock s.m; s.nb_task <- s.nb_task + 1; Mutex.unlock s.m
  let stop s = Mutex.lock s.m; s.nb_task <- s.nb_task - 1;
80
    if s.nb_task = 0 then Condition.signal s.c; Mutex.unlock s.m
81 82 83 84 85 86 87
  let wait s = Mutex.lock s.m; Condition.wait s.c s.m
  let lock s = Mutex.lock s.m
  let unlock s = Mutex.unlock s.m
end

let call s callback tool prob =
  (** Prove goal *)
88 89
  let call q cb task =
    Queue.add (create_proof_attempt ~debug:(Debug.test_flag debug)
90 91
      ~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
      ~command:(tool.tcommand) ~driver:(tool.tdriver)
92 93
      ~callback:cb task) q in
  let iter q pval i task =
94 95 96
    MTask.start s;
    let cb res = callback pval i task res;
      match res with Done _ | InternalFailure _ -> MTask.stop s | _ -> () in
97
    call q cb task; succ i in
98
  let trans_cb pval tl =
99 100 101 102
    let q = Queue.create () in
    ignore (List.fold_left (iter q pval) 0 (List.rev tl));
    transfer_proof_attempts q;
    MTask.stop s in
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
  (** Apply trans *)
  let iter_task (pval,task) =
    MTask.start s;
    let trans = Trans.compose_l prob.ptrans (Trans.singleton tool.ttrans) in
    apply_transformation_l ~callback:(trans_cb pval) trans task in
  (** Split *)
  let ths = prob.ptask tool.tenv tool.tuse in
  MTask.start s;
  List.iter iter_task ths;
  MTask.stop s

let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
  let s = MTask.create () in
  iter (fun v tool prob ->
    let cb pval i task res =
      callback tool.tval pval task i res;
      match res with
        | Done r -> MTask.lock s;
          add v {tool = tool.tval; prob = pval; task = task;
                 idtask = i; result = r};
          MTask.unlock s
        | _ -> () in
    call s cb tool prob);
  MTask.wait s

let any ?callback toolprob =
  let l = ref [] in
  general ?callback (fun f -> List.iter (fun (t,p) -> f () t p) toolprob)
    (fun () r -> l:=r::!l);
  !l


let all_list ?callback tools probs =
  let l = ref [] in
  general ?callback (fun f ->
    List.iter (fun t -> List.iter (fun p -> f () t p) probs) tools)
    (fun () r -> l:=r::!l);
  !l

let all_array ?callback tools probs =
  let m = Array.make_matrix (Array.length tools) (Array.length probs)
    [] in
  general ?callback (fun f ->
    Array.iteri (fun i t -> Array.iteri (fun j p -> f (i,j) t p) probs) tools)
    (fun (i,j) r -> m.(i).(j) <- r::m.(i).(j));
  m