Module Wp.Strategy

module Strategy: sig .. end

val occurs_x : Wp.Lang.F.var -> Wp.Lang.F.term -> bool

val occurs_y : Wp.Lang.F.var -> Wp.Lang.F.pred -> bool

val occurs_e : Wp.Lang.F.term -> Wp.Lang.F.term -> bool

val occurs_p : Wp.Lang.F.term -> Wp.Lang.F.pred -> bool

val occurs_q : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool

val select_e : Wp.Conditions.sequent -> Wp.Lang.F.term -> Wp.Tactical.selection

Lookup the first occurrence of term in the sequent and returns the associated selection. Returns Empty is not found. Goal is lookup first.

val select_p : Wp.Conditions.sequent -> Wp.Lang.F.pred -> Wp.Tactical.selection

Same as select_e but for a predicate.

type argument =

`\|`	`ARG : 'a Wp.Tactical.field * 'a -> argument`

type strategy = {

	`priority : float;`
	`tactical : Wp.Tactical.tactical;`
	`selection : Wp.Tactical.selection;`
	`arguments : argument list;`

}

class pool : object .. end

class type heuristic = object .. end

val register : #heuristic -> unit

val export : #heuristic -> heuristic

val lookup : id:string -> heuristic

val iter : (heuristic -> unit) -> unit

type t = strategy

val arg : 'a Wp.Tactical.field -> 'a -> argument

val make : Wp.Tactical.tactical ->
       ?priority:float ->
       ?arguments:argument list ->
       Wp.Tactical.selection -> strategy