Module Prover

module Prover: sig .. end

val simplify : ?start:(Wpo.t -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
Wpo.t -> bool Task.task
val prove : Wpo.t ->
?config:VCS.config ->
?mode:VCS.mode ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
VCS.prover -> bool Task.task
val spawn : Wpo.t ->
delayed:bool ->
?config:VCS.config ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
?success:(Wpo.t -> VCS.prover option -> unit) ->
?pool:Task.pool -> (VCS.mode * VCS.prover) list -> unit