https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecProvers.mli
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B license *)
(* -------------------------------------------------------------------- *)
open EcPath
(* -------------------------------------------------------------------- *)
type prover_infos = {
pr_maxprocs : int;
pr_provers : string list;
pr_timelimit : int;
pr_wrapper : string option;
}
val dft_prover_infos : prover_infos
val dft_prover_names : string list
val known_provers : unit -> string list
val is_prover_known : string -> bool
(* -------------------------------------------------------------------- *)
val initialize : string option -> unit
(* -------------------------------------------------------------------- *)
type hflag = [ `Include | `Exclude ]
type hints
module Hints : sig
val empty : hints
val full : hints
val add1 : path -> hflag -> hints -> hints
val addm : path -> hflag -> hints -> hints
val mem : path -> hints -> bool
end
(* -------------------------------------------------------------------- *)
val execute_task : prover_infos -> Why3.Task.task -> bool option
val get_w3_th : string list -> string -> Why3.Theory.theory