bench.mli 5.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
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25 26 27 28

open Why
open Env
open Theory
open Task
open Trans
open Driver
open Call_provers
open Scheduler

29 30
module BenchUtil : sig
  val maximum_running_proofs: int ref
31 32 33
(** bound on the number of prover processes running in parallel.
    default is 2 *)

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
  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

72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
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;
90 91 92
  tdriver  : driver;
  tcommand : string;
  tenv     : env;        (** Allow to compare axiomatic easily *)
93
  tuse     : (theory * Db.transf_id option) list;
94 95 96
  ttime    : int;
  tmem     : int;
}
97 98
type gen_task = env -> (theory * Db.transf_id option) list ->
    (prob_id * task) list
99

100
type prob = {
101
  ptask  : gen_task;
102 103
  (** needed for tenv and tuse *)
  ptrans : env -> (task list trans * (Db.transf_id option)) list;
104 105
}

106 107
type why_result =
  | InternalFailure of exn
108
  | Done of  Db.proof_status * float
109

110
val print_why_result : Format.formatter -> why_result -> unit
111 112 113 114 115
type result = {tool   : tool_id;
               prob   : prob_id;
               task   : Decl.prsymbol;
               idtask : int;
               result : why_result}
116

117 118 119 120 121 122
type proof_attempt_status =
  | Runned of why_result
  | Cached of Db.proof_status * float

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

123
type callback = tool_id -> prob_id ->
124
    task -> int -> proof_attempt_status -> unit
125

126
val all_list_tp :
127 128
  ?callback:callback ->
  tool list -> prob list -> result list
129 130

val all_list_pt :
131 132
  ?callback:callback ->
  tool list -> prob list -> result list
133 134

val all_array :
135 136
  ?callback:callback ->
  tool array -> prob array -> result list array array
137 138

val any :
139 140
  ?callback:callback ->
  (tool * prob) list -> result list
141 142 143


val all_list_tools :
144 145
  ?callback:callback ->
  tool list -> prob list -> (tool_id * result list) list
146

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

148 149
type output =
  (** on stdout *)
François Bobot's avatar
François Bobot committed
150 151
  |Average of string
  |Timeline of string
152
  (** In a file *)
François Bobot's avatar
François Bobot committed
153
  |Csv of string
154

155
type bench =
156
    {
François Bobot's avatar
François Bobot committed
157
      bname  : string;
158 159
      btools : tool list;
      bprobs : prob list;
160 161 162 163
      boutputs : output list;
    }

val run_bench :
164
  ?callback:callback -> bench  -> result list
165 166 167


val run_benchs :
168 169
  ?callback:callback -> bench list ->
  (bench * result list) list
170 171

val run_benchs_tools :
172 173
  ?callback:callback -> bench list ->
  (bench * (tool_id * result list) list) list
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188


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

189
val compute_average : result list -> tool_res
190
val compute_timeline :
191 192
  float -> float -> float -> result list -> int list
(** [compute_timeline start end step results] *)
193

194
val filter_timeline : result list -> result list
195

196
val max_time : result list -> float
François Bobot's avatar
François Bobot committed
197 198 199 200

open Format

val print_csv :
201 202 203
  (prob_id -> prob_id -> int)         ->
  (formatter -> tool_id -> unit) ->
  (formatter -> prob_id -> unit) ->
François Bobot's avatar
François Bobot committed
204
  formatter ->
205
  (tool_id * result list) list -> unit
François Bobot's avatar
François Bobot committed
206 207

val print_output :
208 209 210 211
  (prob_id -> prob_id -> int)         ->
  (formatter -> tool_id -> unit) ->
  (formatter -> prob_id -> unit) ->
  bench * (tool_id * result list) list -> unit