Tactic (docs.findlib-94.z3.Z3.Tactic)

type tactic

module ApplyResult : sig ... end

val get_help : tactic -> string

val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs

val apply : 
  tactic ->
  Goal.goal ->
  Params.params option ->
  ApplyResult.apply_result

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