Module ProverWhy3

module ProverWhy3: sig .. end
TODO add them only when needed

None if the po is trivial


val dkey : Log.category
val why3_goal_name : string
val option_file : LogicBuiltins.doption
val option_import : LogicBuiltins.doption
val cluster_file : Definitions.cluster -> string
val theory_name_of_cluster : Definitions.cluster -> string
val theory_name_of_pid : Format.formatter -> WpPropId.prop_id -> unit
type depend = 
| D_file of string
| D_cluster of Definitions.cluster
module TYPES: Model.Index(sig
type key = Lang.adt 
type data = Lang.tau 
val name : string
val compare : Lang.ADT.t -> Lang.ADT.t -> int
val pretty : Format.formatter -> Lang.ADT.t -> unit
end)
val engine : < basename : string -> string; bind : Lang.F.var -> string;
callstyle : Qed.Engine.callstyle; datatype : Lang.ADT.t -> string;
datatypename : string -> string;
declare_axiom : Format.formatter ->
string ->
Lang.F.var list ->
(Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger list list ->
Lang.F.term -> unit;
declare_definition : Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> Lang.F.term -> unit;
declare_fixpoint : prefix:string ->
Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> Lang.F.term -> unit;
declare_prop : kind:string ->
Format.formatter ->
string ->
Lang.F.var list ->
Definitions.trigger list list -> Lang.F.term -> unit;
declare_signature : Format.formatter ->
Lang.F.Fun.t -> Lang.F.tau list -> Lang.F.tau -> unit;
declare_type : Format.formatter ->
Lang.F.ADT.t -> int -> Definitions.typedef -> unit;
e_false : Qed.Engine.cmode -> string; e_true : Qed.Engine.cmode -> string;
field : Lang.Field.t -> string; fieldname : string -> string;
find : Lang.F.var -> string; funname : string -> string;
get_typedef : TYPES.key -> TYPES.data option;
global : (unit -> unit) -> unit; infoprover : 'a. 'a Lang.infoprover -> 'a;
is_atomic : Lang.F.term -> bool; is_shareable : Lang.F.term -> bool;
link : Lang.Fun.t -> Qed.Engine.link; local : (unit -> unit) -> unit;
mode : Qed.Engine.mode; op_add : Qed.Engine.amode -> Qed.Engine.op;
op_and : Qed.Engine.cmode -> Qed.Engine.op;
op_div : Qed.Engine.amode -> Qed.Engine.op;
op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_equal : Qed.Engine.cmode -> Qed.Engine.op;
op_equiv : Qed.Engine.cmode -> Qed.Engine.op;
op_imply : Qed.Engine.cmode -> Qed.Engine.op;
op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_minus : Qed.Engine.amode -> Qed.Engine.op;
op_mod : Qed.Engine.amode -> Qed.Engine.op;
op_mul : Qed.Engine.amode -> Qed.Engine.op;
op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_not : Qed.Engine.cmode -> Qed.Engine.op;
op_noteq : Qed.Engine.cmode -> Qed.Engine.op;
op_or : Qed.Engine.cmode -> Qed.Engine.op; op_real_of_int : Qed.Engine.op;
op_record : string * string; op_scope : Qed.Engine.amode -> string option;
op_spaced : string -> bool; op_sub : Qed.Engine.amode -> Qed.Engine.op;
pp_apply : Qed.Engine.cmode ->
Lang.F.term -> Lang.F.term list Qed.Plib.printer;
pp_array : Lang.F.tau Qed.Plib.printer;
pp_array_get : Format.formatter -> Lang.F.term -> Lang.F.term -> unit;
pp_array_set : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_atom : Lang.F.term Qed.Plib.printer;
pp_conditional : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_cst : Qed.Numbers.cst Qed.Plib.printer;
pp_datatype : Lang.F.ADT.t -> Lang.F.tau list Qed.Plib.printer;
pp_declare_adt : Format.formatter -> Lang.F.ADT.t -> int -> unit;
pp_declare_def : Format.formatter ->
Lang.F.ADT.t -> int -> Lang.F.tau -> unit;
pp_declare_sum : Format.formatter ->
Lang.F.ADT.t ->
int -> (Lang.F.Fun.t * Lang.F.tau list) list -> unit;
pp_declare_symbol : Qed.Engine.cmode -> Lang.F.Fun.t Qed.Plib.printer;
pp_def_fields : (Lang.F.Field.t * Lang.F.term) list Qed.Plib.printer;
pp_equal : Lang.F.term Qed.Plib.printer2;
pp_exists : Lang.F.tau -> string list Qed.Plib.printer;
pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer;
pp_farray : Lang.F.tau Qed.Plib.printer2;
pp_flow : Lang.F.term Qed.Plib.printer;
pp_forall : Lang.F.tau -> string list Qed.Plib.printer;
pp_fun : Qed.Engine.cmode ->
Lang.F.Fun.t -> Lang.F.term list Qed.Plib.printer;
pp_get_field : Format.formatter -> Lang.F.term -> Lang.F.Field.t -> unit;
pp_imply : Format.formatter -> Lang.F.term list -> Lang.F.term -> unit;
pp_int : Qed.Engine.amode -> Lang.F.Z.t Qed.Plib.printer;
pp_intros : Lang.F.tau -> string list Qed.Plib.printer;
pp_lambda : (string * Lang.F.tau) list Qed.Plib.printer;
pp_let : Format.formatter ->
Qed.Engine.pmode -> string -> Lang.F.term -> unit;
pp_not : Lang.F.term Qed.Plib.printer;
pp_noteq : Lang.F.term Qed.Plib.printer2;
pp_param : (string * Lang.F.tau) Qed.Plib.printer;
pp_prop : Lang.F.term Qed.Plib.printer; pp_real : Qed.R.t Qed.Plib.printer;
pp_subtau : Lang.F.tau Qed.Plib.printer;
pp_tau : Lang.F.tau Qed.Plib.printer;
pp_term : Lang.F.term Qed.Plib.printer;
pp_times : Format.formatter -> Lang.F.Z.t -> Lang.F.term -> unit;
pp_trigger : (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
Qed.Plib.printer;
pp_tvar : int Qed.Plib.printer; pp_var : string Qed.Plib.printer;
set_typedef : TYPES.key -> TYPES.data -> unit;
t_atomic : Lang.F.tau -> bool; t_bool : string; t_int : string;
t_prop : string; t_real : string; typeof_call : Lang.lfun -> Lang.tau;
typeof_getfield : Lang.field -> Lang.tau;
typeof_setfield : Lang.field -> Lang.tau;
with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit >
val filenoext : string -> string
val regexp_col : Str.regexp
val regexp_com : Str.regexp
class visitor : Format.formatter -> Definitions.cluster -> object .. end
val write_cluster : Definitions.cluster -> depend list
module CLUSTERS: Model.Index(sig
type key = Definitions.cluster 
type data = int * ProverWhy3.depend list 
val name : string
val compare : Definitions.cluster -> Definitions.cluster -> int
val pretty : Format.formatter -> Definitions.cluster -> unit
end)
val assemble_cluster : depend -> unit
val assemble_goal : title:string ->
id:string ->
pid:WpPropId.prop_id ->
axioms:Definitions.axioms option -> Lang.F.pred -> Format.formatter -> unit
module FunFile: Model.Index(sig
type key = Cil_types.kernel_function 
type data = int 
val name : string
val compare : Kernel_function.t -> Kernel_function.t -> int
val pretty : Format.formatter -> Kernel_function.t -> unit
end)
type goal_id = {
   gfile : string;
   gtheory : string;
   ggoal : string;
}
val assemble_wpo : Wpo.t -> (string list * goal_id) option
None if the po is trivial
val assemble_check : Wpo.t -> Wpo.VC_Check.t -> string list * goal_id
val assemble_wpo : Wpo.t -> (string list * goal_id) option
None if the po is trivial
val p_goal : string
val p_valid : string
val p_unknown : string
val p_limit : string
val p_error : string
val re_valid : Str.regexp
val re_unknown : Str.regexp
val re_limit : Str.regexp
val re_error : Str.regexp
type error = 
| Error_No
| Error_Prover of string
| Error_Generated of Lexing.position * string
val split : string -> int -> string list
val chop_version : string -> string
class why3 : prover:string -> pid:'a -> file:goal_id -> includes:string list -> logout:string -> logerr:string -> object .. end
val prove_file : prover:string ->
pid:'a ->
file:goal_id ->
includes:string list ->
logout:string -> logerr:string -> VCS.result Task.task
val prove_prop : prover:string -> wpo:Wpo.t -> VCS.result Task.task
val prove : Wpo.t -> prover:string -> VCS.result Task.task
The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed
class why3ide : includes:string list -> files:Wp_parameters.WhyFlags.t -> session:string -> object .. end
val call_ide : includes:string list ->
files:Wp_parameters.WhyFlags.t -> session:string -> bool Task.task
type dp = {
   dp_name : string;
   dp_version : string;
   dp_prover : string;
}
val find : string -> dp list -> dp
val parse : string -> dp
val pe_prover : Str.regexp
class why3detect : (dp list option -> unit) -> object .. end
val detect_why3 : (dp list option -> unit) -> unit
val detect_provers : (dp list -> unit) -> unit