sig
val env : Conditions.sequent -> Repr.env
val occurs_x : Lang.F.var -> Lang.F.term -> bool
val occurs_y : Lang.F.var -> Lang.F.pred -> bool
val occurs_e : Lang.F.term -> Lang.F.term -> bool
val occurs_p : Lang.F.term -> Lang.F.pred -> bool
val occurs_q : Lang.F.pred -> Lang.F.pred -> bool
val select_e : Conditions.sequent -> Lang.F.term -> Tactical.selection
val select_p : Conditions.sequent -> Lang.F.pred -> Tactical.selection
type argument = ARG : 'a Tactical.field * 'a -> Strategy.argument
type strategy = {
priority : float;
tactical : Tactical.tactical;
selection : Tactical.selection;
arguments : Strategy.argument list;
}
class pool :
object
method add : Strategy.strategy -> unit
method sort : Strategy.strategy array
end
class type heuristic =
object
method descr : string
method id : string
method search :
(Strategy.strategy -> unit) -> Conditions.sequent -> unit
method title : string
end
val register : #Strategy.heuristic -> unit
val export : #Strategy.heuristic -> Strategy.heuristic
val lookup : id:string -> Strategy.heuristic
val iter : (Strategy.heuristic -> unit) -> unit
type t = Strategy.strategy
val arg : 'a Tactical.field -> 'a -> Strategy.argument
val make :
Tactical.tactical ->
?priority:float ->
?arguments:Strategy.argument list ->
Tactical.selection -> Strategy.strategy
val set_arg : Tactical.tactical -> Strategy.argument -> unit
val set_args : Tactical.tactical -> Strategy.argument list -> unit
end