ProverScript (frama-c-wp.Wp.ProverScript)

type 'a process =
  ?valid:bool ->
  ?failed:bool ->
  ?scratch:bool ->
  ?provers:VCS.prover list ->
  ?depth:int ->
  ?width:int ->
  ?backtrack:int ->
  ?auto:Strategy.heuristic list ->
  ?strategies:bool ->
  ?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)
scratch: Discard existing script (default: false)
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 Frama_c_kernel.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 explore : 
  ?depth:int ->
  ?strategy:ProofStrategy.strategy ->
  ?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 -> [ `Script | `Proof | `Saved | `None ]