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

val first : 
  ProofEngine.tree ->
  ?anchor:ProofEngine.node ->
  Strategy.t array ->
  ProofEngine.fork option

val index : 
  ProofEngine.tree ->
  anchor:ProofEngine.node ->
  index:int ->
  ProofEngine.fork option

val search : 
  ProofEngine.tree ->
  ?anchor:ProofEngine.node ->
  ?sequent:Conditions.sequent ->
  Strategy.heuristic list ->
  ProofEngine.fork option

val backtrack : 
  ProofEngine.tree ->
  ?anchor:ProofEngine.node ->
  ?loop:bool ->
  ?width:int ->
  unit ->
  ProofEngine.fork option