sig
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
val select_p :
Wp.Conditions.sequent -> Wp.Lang.F.pred -> Wp.Tactical.selection
type argument = ARG : 'a Wp.Tactical.field * 'a -> Wp.Strategy.argument
type strategy = {
priority : float;
tactical : Wp.Tactical.tactical;
selection : Wp.Tactical.selection;
arguments : Wp.Strategy.argument list;
}
class pool :
object
method add : Wp.Strategy.strategy -> unit
method sort : Wp.Strategy.strategy array
end
class type heuristic =
object
method descr : string
method id : string
method search :
(Wp.Strategy.strategy -> unit) -> Wp.Conditions.sequent -> unit
method title : string
end
val register : #Wp.Strategy.heuristic -> unit
val export : #Wp.Strategy.heuristic -> Wp.Strategy.heuristic
val lookup : id:string -> Wp.Strategy.heuristic
val iter : (Wp.Strategy.heuristic -> unit) -> unit
type t = Wp.Strategy.strategy
val arg : 'a Wp.Tactical.field -> 'a -> Wp.Strategy.argument
val make :
Wp.Tactical.tactical ->
?priority:float ->
?arguments:Wp.Strategy.argument list ->
Wp.Tactical.selection -> Wp.Strategy.strategy
val set_arg : Wp.Tactical.tactical -> Wp.Strategy.argument -> unit
val set_args : Wp.Tactical.tactical -> Wp.Strategy.argument list -> unit
end