Skip to main content

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: