module ProverScript:sig
..end
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
- valid
: Play provers with valid result (default: true)
failed
: Play provers with invalid result (default: true)provers
: Additional list of provers to try when stuckdepth
: Strategy search depth (default: 0)width
: Strategy search width (default: 0)backtrack
: Strategy backtracking (default: 0)auto
: Strategies to try (default: none)val prove : unit Task.task process
val spawn : unit 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 : stdout:bool -> Wpo.t -> unit