# Strategies

High-performance solvers, such as Z3, contain many tightly integrated, handcrafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform very badly on new classes of problems. This issue is becoming increasingly pressing as solvers begin to gain the attention of practitioners in diverse areas of science and engineering. In many cases, changes to the solver heuristics can make a tremendous difference.

In this tutorial we show how to create custom strategies using the basic building blocks available in Z3. Z3 implement the ideas proposed in this article.

## Introduction

Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic reasoning steps are represented as functions known as tactics, and tactics are composed using combinators known as tacticals. Tactics process sets of formulas called Goals.

When a tactic is applied to some goal G, four different outcomes are possible. In SMT 2.0, the goal is the conjunction of all assertions. The tactic succeeds in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.

In the following example, we use the command apply to execute a tactic composed of two built-in tactics: simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted only to linear arithmetic. It can also eliminate arbitrary variables. Then, combinator then applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. In this example, only one subgoal is produced.

```(declare-const x Real)
(declare-const y Real)

(assert (> x 0.0))
(assert (> y 0.0))
(assert (= x (+ y 2.0)))

(apply (then simplify solve-eqs))```

In the example above, variable x is eliminated, and is not present the resultant goal.

In Z3, we say a clause is any constraint of the form (or f_1 ... f_n). The tactic split-clause will select a clause (or f_1 ... f_n) in the input goal, and split it n subgoals. One for each subformula f_i.

```(declare-const x Real)
(declare-const y Real)

(assert (or (< x 0.0) (> x 0.0)))
(assert (= x (+ y 1.0)))
(assert (< y 0.0))

(apply split-clause)```

## Tactics

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

`(help-tactic)`

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 tractic 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 millisenconds, 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.

```(declare-const x Real)
(declare-const y Real)
(declare-const z Real)

(assert (or (= x 0.0) (= x 1.0)))
(assert (or (= y 0.0) (= y 1.0)))
(assert (or (= z 0.0) (= z 1.0)))
(assert (> (+ x y z) 2.0))

(echo "split all...")
(apply (repeat (or-else split-clause skip)))

(echo "split at most 2...")
(apply (repeat (or-else split-clause skip) 1))

(echo "split and solve-eqs...")
(apply (then (repeat (or-else split-clause skip)) solve-eqs))```

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.

```(declare-const x (_ BitVec 16))
(declare-const y (_ BitVec 16))

(assert (= (bvor x y) (_ bv13 16)))
(assert (bvslt x y))

(check-sat-using (then simplify solve-eqs bit-blast sat))
(get-model)```

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.

```(declare-const x (_ BitVec 16))
(declare-const y (_ BitVec 16))

(assert (= (bvadd (bvmul (_ bv32 16) x) y) (_ bv13 16)))
(assert (bvslt (bvand x y) (_ bv10 16)))
(assert (bvsgt y (bvneg (_ bv100 16))))

(check-sat-using (then (using-params simplify :mul2concat true)
solve-eqs
bit-blast
aig
sat))
(get-model)
(get-value ((bvand x y)))```

The tactic smt wraps the main solver in Z3 as a tactic.

```(declare-const x Int)
(declare-const y Int)

(assert (> x (+ y 1)))

(check-sat-using smt)
(get-model)```

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.

```(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (and (> x 0) (< x 10)))
(assert (and (> y 0) (< y 10)))
(assert (and (> z 0) (< z 10)))
(assert (= (+ (* 3 y) (* 2 x)) z))

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
normalize-bounds
lia2pb
pb2bv
bit-blast
sat))
(get-model)

(reset)

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (= (+ (* 3 y) (* 2 x)) z))

;; The next command will fail since x, y and z are not bounded.
(check-sat-using (then (using-params simplify :arith-lhs true :som true)
normalize-bounds
lia2pb
pb2bv
bit-blast
sat))
(get-info :reason-unknown)```

The next example demonstrates how to run different strategies in parallel using the combinator par-or. It also shows how to run different instances of the smt tactic using different random seeds.

```(declare-const x (_ BitVec 64))
(declare-const y (_ BitVec 64))
(declare-const z (_ BitVec 64))

(assert (bvsgt x (_ bv10 64)))
(assert (= x y))
(assert (= y (bvadd z z)))

(check-sat-using
(par-or
;; Strategy 1: use bit-blasting
(then simplify bit-blast sat)
;; Strategy 2: use default solver
smt))

(get-model)

(echo "using different random seeds...")

(check-sat-using
(par-or
;; Strategy 1: using seed 1
(using-params smt :random-seed 1)
;; Strategy 1: using seed 2
(using-params smt :random-seed 2)
;; Strategy 1: using seed 3
(using-params smt :random-seed 3)))

(get-model)```

## 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.

`(help-tactic)`

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.

```(declare-const x Real)
(declare-const y Real)
(declare-const z Real)

(push)
(assert (> (+ x y z) 0.0))

(apply (echo "num consts: " num-consts))

(apply (fail-if (> num-consts 2)))
(pop)

(echo "trying again...")
(assert (> (+ x y) 0.0))
(apply (fail-if (> num-consts 2)))```

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.

```(declare-const x Real)