ecProvers.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcPath
(* -------------------------------------------------------------------- *)
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
(* -------------------------------------------------------------------- *)
type prover_eviction = [
| `Inconsistent
]
type prover = {
pr_name : string;
pr_version : string;
pr_evicted : (prover_eviction * bool) option;
}
type prover_infos = {
pr_maxprocs : int;
pr_provers : string list;
pr_timelimit : int;
pr_cpufactor : int;
pr_quorum : int;
pr_wrapper : string option;
pr_verbose : int;
pr_all : bool;
pr_max : int;
pr_iterate : bool;
pr_wanted : hints;
pr_unwanted : hints;
pr_selected : bool;
}
val dft_prover_infos : prover_infos
val dft_prover_names : string list
val known : evicted:bool -> prover list
(* -------------------------------------------------------------------- *)
type parsed_pname = {
prn_name : string;
prn_ovrevict : bool;
}
val parse_prover_name : string -> parsed_pname
val is_prover_known : string -> bool
(* -------------------------------------------------------------------- *)
val initialize :
?ovrevict:string list
-> ?why3conf:string
-> unit -> unit
(* -------------------------------------------------------------------- *)
type notify = EcGState.loglevel -> string Lazy.t -> unit
val execute_task : ?notify:notify -> prover_infos -> Why3.Task.task -> bool option
val get_w3_th : string list -> string -> Why3.Theory.theory