module Tactic:sig
..end
Tactics are the basic building block for creating custom solvers for specific problem domains.
The complete list of tactics may be obtained using Context.get_num_tactics
and Context.get_tactic_names
.
It may also be obtained using the command (help-tactics)
in the SMT 2.0 front-end.
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
If the tactic does not terminate within the timeout, then it fails.
val when_ : context -> Probe.probe -> tactic -> tactic
If the probe evaluates to false, then the new tactic behaves like the skip
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
UsingParams
val par_or : context -> tactic list -> tactic
val par_and_then : context -> tactic -> tactic -> tactic
val interrupt : context -> unit