Wp.ProofStrategy
val name : strategy -> string
val loc : strategy -> Frama_c_kernel.Cil_types.location
val find : string -> strategy option
val hints : ?node:ProofEngine.node -> Wpo.t -> strategy list
val has_hint : Wpo.t -> bool
val iter : (strategy -> unit) -> unit
val default : unit -> strategy list
val alternatives : strategy -> alternative list
val provers :
?default:VCS.prover list ->
alternative ->
VCS.prover list * float
val auto : alternative -> Strategy.heuristic option
val fallback : alternative -> strategy option
val tactic :
ProofEngine.tree ->
ProofEngine.node ->
strategy ->
alternative ->
ProofEngine.node list option
val pp_strategy : Stdlib.Format.formatter -> strategy -> unit
val pp_alternative : Stdlib.Format.formatter -> alternative -> unit