Probes

Probes (aka formula measures) are evaluated over goals. Boolean expressions over them can be built using relational operators and Boolean connectives. The tactic (fail-if cond) fails if the given goal does not satisfy the condition cond. Many numeric and Boolean measures are available in Z3. The command (help-tactic) provides the list of all built-in probes.

In the following example, we build a simple tactic using fail-if. It also shows that echo can be used to display the value returned by a probe. The echo tactic is mainly used for debugging purposes.

Z3 also provides the combinator (tactical) (if p t1 t2) which is a shorthand for:

(or-else (then (fail-if (not p)) t1) t2)

The combinator (when p t) is a shorthand for:

(if p t skip)

The tactic skip just returns the input goal. The following example demonstrates how to use the if combinator.