# Tactics

Z3 comes equipped with many built-in tactics. The command (help-tactic) provides a short description of all built-in tactics.

Z3 comes equipped with the following tactic combinators (aka tacticals):

`(then t s)`

applies /t to the input goal and /s to every subgoal produced by /t.`(par-then t s)`

applies /t to the input goal and /s to every subgoal produced by /t in parallel.`(or-else t s)`

first applies /t to the given goal, if it fails then returns the result of /s applied to the given goal.`(par-or t s)`

applies /t and /s in parallel until one of them succeed. The tactic fails if /t and /s fails.`(repeat t)`

Keep applying the given tactic until no subgoal is modified by it.`(repeat t n)`

Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than /n.`(try-for t ms)`

Apply tactic /t to the input goal, if it does not return in /ms milliseconds, it fails.`(using-params t params)`

Apply the given tactic using the given parameters.`(! t params)`

is a shorthand for`(using-params t params)`

.

The combinators `then`

, `par-then`

, `or-else`

and `par-or`

accept arbitrary number of arguments. The following example demonstrate how to use these combinators.

In the last apply command, the tactic `solve-eqs`

discharges all but one goal. Note that, this tactic generates one goal: the empty goal which is trivially satisfiable (i.e., feasible)

A tactic can be used to decide whether a set of assertions has a solution (i.e., is satisfiable) or not. The command `check-sat-using`

is similar to `check-sat`

, but uses the given tactic instead of the Z3 default solver for solving the current set of assertions. If the tactic produces the empty goal, then check-sat-using returns sat. If the tactic produces a single goal containing `False`

, then `check-sat-using`

returns `unsat`

. Otherwise, it returns `unknown`

.

In the example above, the tactic used implements a basic bit-vector solver using equation solving, bit-blasting, and a propositional SAT solver.

In the following example, we use the combinator using-params to configure our little solver. We also include the tactic `aig`

which tries to compress Boolean formulas using And-Inverted Graphs.

The tactic `smt`

wraps the main solver in Z3 as a tactic:

We now show how to implement a solver for integer arithmetic using SAT. The solver is complete only for problems where every variable has a lower and upper bound: