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: