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 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 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 ]