bench.mli 5.04 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Why3
13 14 15 16 17 18
open Env
open Theory
open Task
open Trans
open Driver

19 20
module BenchUtil : sig
  val maximum_running_proofs: int ref
21 22 23
(** bound on the number of prover processes running in parallel.
    default is 2 *)

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
  val new_external_proof :
    Call_provers.pre_prover_call * (Call_provers.prover_result -> unit)
    -> unit
  (** [new_external_proof pre_prover_call callback] *)

  val wait_remaining_task : unit -> unit
  (** Wait the completion of the remaining task started by
      new_external_proof *)

  val task_checksum : Task.task -> string

  val apply_trans :
    task * Db.goal option ->
    task trans * Db.transf_id option ->
    task * Db.goal option
  (** [apply_transl trans goal] *)

  val apply_transl :
    task * Db.goal option ->
    task list trans * Db.transf_id option ->
    (task * Db.goal option) list
  (** [apply_transl transl goal] *)

  val apply_transll :
    (task list trans * Db.transf_id option) list ->
    (task * Db.goal option) list ->
    task * Db.goal option ->
    (task * Db.goal option) list
  (** [apply_transll transllist acc goal] *)

  val proof_status_to_db_result :
    Call_provers.prover_result -> Db.proof_status * float

  val print_proof_status :
    Format.formatter -> Db.proof_status -> unit

end

62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
type tool_id = {
  tool_name : string;
  prover_name : string;
  tool_db : Db.prover_id option;
  }
(* tool_name, prover_name *)

type prob_id = {
  prob_name : string;
  prob_file : string;
  prob_theory : string;
  prob_db : Db.goal option;
}
(* prob_name, file_name, theory name *)

type tool = {
  tval     : tool_id;
  ttrans   : (task trans * (Db.transf_id option)) list;
80 81 82
  tdriver  : driver;
  tcommand : string;
  tenv     : env;        (** Allow to compare axiomatic easily *)
83
  tuse     : (theory * Db.transf_id option) list;
84 85 86
  ttime    : int;
  tmem     : int;
}
87 88
type gen_task = env -> (theory * Db.transf_id option) list ->
    (prob_id * task) list
89

90
type prob = {
91
  ptask  : gen_task;
92 93
  (** needed for tenv and tuse *)
  ptrans : env -> (task list trans * (Db.transf_id option)) list;
94 95
}

96 97
type why_result =
  | InternalFailure of exn
98
  | Done of  Db.proof_status * float
99

100
val print_why_result : Format.formatter -> why_result -> unit
101 102 103 104 105
type result = {tool   : tool_id;
               prob   : prob_id;
               task   : Decl.prsymbol;
               idtask : int;
               result : why_result}
106

107 108 109 110 111 112
type proof_attempt_status =
  | Runned of why_result
  | Cached of Db.proof_status * float

val print_pas : Format.formatter -> proof_attempt_status -> unit

113
type callback = tool_id -> prob_id ->
114
    task -> int -> proof_attempt_status -> unit
115

116
val all_list_tp :
117 118
  ?callback:callback ->
  tool list -> prob list -> result list
119 120

val all_list_pt :
121 122
  ?callback:callback ->
  tool list -> prob list -> result list
123 124

val all_array :
125 126
  ?callback:callback ->
  tool array -> prob array -> result list array array
127 128

val any :
129 130
  ?callback:callback ->
  (tool * prob) list -> result list
131 132 133


val all_list_tools :
134 135
  ?callback:callback ->
  tool list -> prob list -> (tool_id * result list) list
136

François Bobot's avatar
François Bobot committed
137

138
type output =
François Bobot's avatar
François Bobot committed
139
  (** In a file *)
François Bobot's avatar
François Bobot committed
140 141 142
  |Average of string
  |Timeline of string
  |Csv of string
143

144
type bench =
145
    {
François Bobot's avatar
François Bobot committed
146
      bname  : string;
147 148
      btools : tool list;
      bprobs : prob list;
149 150 151 152
      boutputs : output list;
    }

val run_bench :
153
  ?callback:callback -> bench  -> result list
154 155 156


val run_benchs :
157 158
  ?callback:callback -> bench list ->
  (bench * result list) list
159 160

val run_benchs_tools :
161 162
  ?callback:callback -> bench list ->
  (bench * (tool_id * result list) list) list
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177


type nb_avg = int * float

val print_nb_avg : Format.formatter -> nb_avg -> unit

type tool_res =
    { valid : nb_avg;
      timeout : nb_avg;
      unknown : nb_avg;
      invalid : nb_avg;
      failure : nb_avg}

val print_tool_res : Format.formatter -> tool_res -> unit

178
val compute_average : result list -> tool_res
179
val compute_timeline :
180 181
  float -> float -> float -> result list -> int list
(** [compute_timeline start end step results] *)
182

183
val filter_timeline : result list -> result list
184

185
val max_time : result list -> float
François Bobot's avatar
François Bobot committed
186 187 188 189

open Format

val print_csv :
190 191 192
  (prob_id -> prob_id -> int)         ->
  (formatter -> tool_id -> unit) ->
  (formatter -> prob_id -> unit) ->
François Bobot's avatar
François Bobot committed
193
  formatter ->
194
  (tool_id * result list) list -> unit
François Bobot's avatar
François Bobot committed
195 196

val print_output :
197 198 199 200
  (prob_id -> prob_id -> int)         ->
  (formatter -> tool_id -> unit) ->
  (formatter -> prob_id -> unit) ->
  bench * (tool_id * result list) list -> unit