sig
type t
val get_id : Wp.VC.t -> string
val get_model : Wp.VC.t -> Wp.WpContext.model
val get_scope : Wp.VC.t -> Wp.WpContext.scope
val get_context : Wp.VC.t -> Wp.WpContext.context
val get_description : Wp.VC.t -> string
val get_property : Wp.VC.t -> Property.t
val get_result : Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result
val get_results : Wp.VC.t -> (Wp.VCS.prover * Wp.VCS.result) list
val get_logout : Wp.VC.t -> Wp.VCS.prover -> string
val get_logerr : Wp.VC.t -> Wp.VCS.prover -> string
val get_sequent : Wp.VC.t -> Wp.Conditions.sequent
val get_formula : Wp.VC.t -> Wp.Lang.F.pred
val is_trivial : Wp.VC.t -> bool
val is_proved : Wp.VC.t -> bool
val clear : unit -> unit
val proof : Property.t -> Wp.VC.t list
val remove : Property.t -> unit
val iter_ip : (Wp.VC.t -> unit) -> Property.t -> unit
val iter_kf :
(Wp.VC.t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
val generate_ip : ?model:string -> Property.t -> Wp.VC.t Bag.t
val generate_kf :
?model:string ->
?bhv:string list ->
?prop:string list -> Kernel_function.t -> Wp.VC.t Bag.t
val generate_call : ?model:string -> Cil_types.stmt -> Wp.VC.t Bag.t
val prove :
Wp.VC.t ->
?config:Wp.VCS.config ->
?mode:Wp.VCS.mode ->
?start:(Wp.VC.t -> unit) ->
?progress:(Wp.VC.t -> string -> unit) ->
?result:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
Wp.VCS.prover -> bool Task.task
val spawn :
Wp.VC.t ->
?config:Wp.VCS.config ->
?start:(Wp.VC.t -> unit) ->
?progress:(Wp.VC.t -> string -> unit) ->
?result:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
?success:(Wp.VC.t -> Wp.VCS.prover option -> unit) ->
?pool:Task.pool -> (Wp.VCS.mode * Wp.VCS.prover) list -> unit
val server : ?procs:int -> unit -> Task.server
val command :
?provers:Why3.Whyconf.prover list -> ?tip:bool -> Wp.VC.t Bag.t -> unit
end