Module Z3.Tactic

module Tactic: sig .. end

Tactics

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-tactic) in the SMT 2.0 front-end.

type tactic

module ApplyResult: sig .. end

Tactic application results

val get_help : tactic -> string

A string containing a description of parameters accepted by the tactic.

val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs

Retrieves parameter descriptions for Tactics.

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

Apply the tactic to the goal.

val get_num_tactics : context -> int

The number of supported tactics.

val get_tactic_names : context -> string list

The names of all supported tactics.

val get_tactic_description : context -> string -> string

Returns a string containing a description of the tactic with the given name.

val mk_tactic : context -> string -> tactic

Creates a new Tactic.

val and_then : context ->
       tactic ->
       tactic -> tactic list -> tactic

Create a tactic that applies one tactic to a Goal and then another one to every subgoal produced by the first one.

val or_else : context -> tactic -> tactic -> tactic

Create a tactic that first applies one tactic to a Goal and if it fails then returns the result of another tactic applied to the Goal.

val try_for : context -> tactic -> int -> tactic

Create a tactic that applies one tactic to a goal for some time (in milliseconds).

If the tactic does not terminate within the timeout, then it fails.

val when_ : context -> Probe.probe -> tactic -> tactic

Create a tactic that applies one tactic to a given goal if the probe evaluates to true.

If the probe evaluates to false, then the new tactic behaves like the skip tactic.

val cond : context ->
       Probe.probe -> tactic -> tactic -> tactic

Create a tactic that applies a tactic to a given goal if the probe evaluates to true and another tactic otherwise.

val repeat : context -> tactic -> int -> tactic

Create a tactic that keeps applying one tactic until the goal is not modified anymore or the maximum number of iterations is reached.

val skip : context -> tactic

Create a tactic that just returns the given goal.

val fail : context -> tactic

Create a tactic always fails.

val fail_if : context -> Probe.probe -> tactic

Create a tactic that fails if the probe evaluates to false.

val fail_if_not_decided : context -> tactic

Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').

val using_params : context -> tactic -> Params.params -> tactic

Create a tactic that applies a tactic using the given set of parameters.

val with_ : context -> tactic -> Params.params -> tactic

Create a tactic that applies a tactic using the given set of parameters. Alias for UsingParams

val par_or : context -> tactic list -> tactic

Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).

val par_and_then : context -> tactic -> tactic -> tactic

Create a tactic that applies a tactic to a given goal and then another tactic to every subgoal produced by the first one. The subgoals are processed in parallel.

val interrupt : context -> unit

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.