Module ProverScript

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 stuck
depth: 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