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).
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
unsat. Otherwise, it returns
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.
smt wraps the main solver in Z3 as a tactic.
Now, we 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.