sig
type prover = Why3 of string | AltErgo | Coq | Qed | Tactical
type mode = BatchMode | EditMode | FixMode
type language = L_why3 | L_coq | L_altergo
module Pset :
sig
type elt = prover
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> t
end
module Pmap :
sig
type key = prover
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_first : (key -> bool) -> 'a t -> key * 'a
val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
val find_last : (key -> bool) -> 'a t -> key * 'a
val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Seq.t -> 'a t
end
val language_of_prover : VCS.prover -> VCS.language
val name_of_prover : VCS.prover -> string
val title_of_prover : VCS.prover -> string
val filename_for_prover : VCS.prover -> string
val prover_of_name : string -> VCS.prover option
val language_of_prover_name : string -> VCS.language option
val mode_of_prover_name : string -> VCS.mode
val title_of_mode : VCS.mode -> string
val pp_prover : Stdlib.Format.formatter -> VCS.prover -> unit
val pp_language : Stdlib.Format.formatter -> VCS.language -> unit
val pp_mode : Stdlib.Format.formatter -> VCS.mode -> unit
val cmp_prover : VCS.prover -> VCS.prover -> int
type dp = {
dp_name : string;
dp_version : string;
dp_altern : string;
dp_shortcuts : string list;
}
val prover_of_dp : VCS.dp -> VCS.prover
val pretty : Stdlib.Format.formatter -> VCS.dp -> unit
val pp_shortcut : Stdlib.Format.formatter -> string -> unit
val pp_shortcuts : Stdlib.Format.formatter -> string list -> unit
type config = {
valid : bool;
timeout : int option;
stepout : int option;
depth : int option;
}
val current : unit -> VCS.config
val default : VCS.config
val get_timeout : VCS.config -> int
val get_stepout : VCS.config -> int
val get_depth : VCS.config -> int
type verdict =
NoResult
| Invalid
| Unknown
| Timeout
| Stepout
| Computing of (unit -> unit)
| Checked
| Valid
| Failed
type result = {
verdict : VCS.verdict;
solver_time : float;
prover_time : float;
prover_steps : int;
prover_depth : int;
prover_errpos : Stdlib.Lexing.position option;
prover_errmsg : string;
}
val no_result : VCS.result
val valid : VCS.result
val checked : VCS.result
val invalid : VCS.result
val unknown : VCS.result
val stepout : VCS.result
val timeout : int -> VCS.result
val computing : (unit -> unit) -> VCS.result
val failed : ?pos:Stdlib.Lexing.position -> string -> VCS.result
val kfailed :
?pos:Stdlib.Lexing.position ->
('a, Stdlib.Format.formatter, unit, VCS.result) Stdlib.format4 -> 'a
val result :
?solver:float ->
?time:float -> ?steps:int -> ?depth:int -> VCS.verdict -> VCS.result
val is_auto : VCS.prover -> bool
val is_verdict : VCS.result -> bool
val is_valid : VCS.result -> bool
val configure : VCS.result -> VCS.config
val autofit : VCS.result -> bool
val pp_result : Stdlib.Format.formatter -> VCS.result -> unit
val pp_result_perf : Stdlib.Format.formatter -> VCS.result -> unit
val compare : VCS.result -> VCS.result -> int
val merge : VCS.result -> VCS.result -> VCS.result
val choose : VCS.result -> VCS.result -> VCS.result
val best : VCS.result list -> VCS.result
val dkey_no_time_info : Wp_parameters.category
val dkey_no_step_info : Wp_parameters.category
val dkey_no_goals_info : Wp_parameters.category
val dkey_success_only : Wp_parameters.category
end