sig
val array : ?priority:float -> Tactical.selection -> Strategy.strategy
val choice : ?priority:float -> Tactical.selection -> Strategy.strategy
val absurd : ?priority:float -> Tactical.selection -> Strategy.strategy
val contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy
val compound : ?priority:float -> Tactical.selection -> Strategy.strategy
val cut :
?priority:float -> ?modus:bool -> Tactical.selection -> Strategy.strategy
val filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy
val havoc :
?priority:float -> havoc:Tactical.selection -> Strategy.strategy
val separated : ?priority:float -> Tactical.selection -> Strategy.strategy
val instance :
?priority:float ->
Tactical.selection -> Tactical.selection list -> Strategy.strategy
val lemma :
?priority:float ->
?at:Tactical.selection ->
string -> Tactical.selection list -> Strategy.strategy
val intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
val range :
?priority:float ->
Tactical.selection -> vmin:int -> vmax:int -> Strategy.strategy
val split : ?priority:float -> Tactical.selection -> Strategy.strategy
val definition : ?priority:float -> Tactical.selection -> Strategy.strategy
val auto_split : Strategy.heuristic
val auto_range : Strategy.heuristic
module Range :
sig
type rg
val compute : Conditions.sequence -> Auto.Range.rg
val ranges : Auto.Range.rg -> (int * int) Lang.F.Tmap.t
val bounds : Auto.Range.rg -> (int option * int option) Lang.F.Tmap.t
end
val t_absurd : Tactical.process
val t_id : Tactical.process
val t_finally : string -> Tactical.process
val t_descr : string -> Tactical.process -> Tactical.process
val t_split : ?pos:string -> ?neg:string -> Lang.F.pred -> Tactical.process
val t_cut :
?by:string -> Lang.F.pred -> Tactical.process -> Tactical.process
val t_case :
Lang.F.pred -> Tactical.process -> Tactical.process -> Tactical.process
val t_cases :
?complete:string ->
(Lang.F.pred * Tactical.process) list -> Tactical.process
val t_chain : Tactical.process -> Tactical.process -> Tactical.process
val t_range :
Lang.F.term ->
int ->
int ->
upper:Tactical.process ->
lower:Tactical.process -> range:Tactical.process -> Tactical.process
val t_replace :
?equal:string ->
src:Lang.F.term ->
tgt:Lang.F.term -> Tactical.process -> Tactical.process
end