sig
type 'a process =
?valid:bool ->
?failed:bool ->
?provers:VCS.prover list ->
?depth:int ->
?width:int ->
?backtrack:int ->
?auto:Strategy.heuristic list ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
?success:(Wpo.t -> VCS.prover option -> unit) -> Wpo.t -> 'a
val prove : unit Task.task ProverScript.process
val spawn : unit ProverScript.process
val search :
?depth:int ->
?width:int ->
?backtrack:int ->
?auto:Strategy.heuristic list ->
?provers:VCS.prover list ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
?success:(Wpo.t -> VCS.prover option -> unit) ->
ProofEngine.tree -> ProofEngine.node -> unit
val get : Wpo.t -> [ `None | `Proof | `Saved | `Script ]
val save : Wpo.t -> unit
end