package z3

  1. Overview
  2. Docs
type tactic
module ApplyResult : sig ... end
val get_help : tactic -> string
val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs
val get_num_tactics : context -> int
val get_tactic_names : context -> string list
val get_tactic_description : context -> string -> string
val mk_tactic : context -> string -> tactic
val and_then : context -> tactic -> tactic -> tactic list -> tactic
val or_else : context -> tactic -> tactic -> tactic
val try_for : context -> tactic -> int -> tactic
val when_ : context -> Probe.probe -> tactic -> tactic
val cond : context -> Probe.probe -> tactic -> tactic -> tactic
val repeat : context -> tactic -> int -> tactic
val skip : context -> tactic
val fail : context -> tactic
val fail_if : context -> Probe.probe -> tactic
val fail_if_not_decided : context -> tactic
val using_params : context -> tactic -> Params.params -> tactic
val with_ : context -> tactic -> Params.params -> tactic
val par_or : context -> tactic list -> tactic
val par_and_then : context -> tactic -> tactic -> tactic
val interrupt : context -> unit