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.
Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
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.
load in editor(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.
load in editor(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)
Z3 comes equipped with many built-in tactics. The command (help-tactic) provides a short description of all built-in tactics.
load in editor(help-tactic)
Z3 comes equipped with the following tactic combinators (aka tacticals):
The combinators then, par-then, or-else and par-or accept arbitrary number of arguments. The following example demonstrate how to use these combinators.
load in editor(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.
load in editor(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.
load in editor(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.
load in editor(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.
load in editor(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.
load in editor(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 (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.
load in editor(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.
load in editor(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.
load in editor(declare-const x Real) (declare-const y Real) (declare-const z Real) (assert (>= (- (^ x 2.0) (^ y 2.0)) 0.0)) (apply (if (> num-consts 2) simplify factor)) (assert (>= (+ x x y z) 0.0)) (apply (if (> num-consts 2) simplify factor))