# Programming Constraint Services with Z3

## A tutorial - Automata, Logic and Games, NUS

 Nikolaj Bjørner Microsoft Research nbjorner@microsoft.com

## Overview

Goal of this tutorial is to give an overview of what you can do with Z3 from the perspectives of:

• What is expressible: Logics and Theories.

• Adaptability: Mapping logical queries to Z3.

• Programmability: using the API.

• Efficiency: Algorithms.

## Z3

• A state-of-art Satisfiability Modulo Theories (SMT) solver from Microsoft Research

• Targets applications in software engineering

• Leonardo de Moura, Nikolaj Bjørner, and Christoph Wintersteiger

• Contributions from Ken McMillan, Mikolas Janota, Loris d'Antoni, George Karpenkov, Dan Lieuw and several others
• Contributions are solicited
• On github: https://github.com/Z3prover/z3.git

• MIT open source license

## Logics and Theories

 Terms Logical Connectives Quantifiers, Variables Propositional logic Theory of Equality Uninterpreted Functions Arrays Arithmetic Arrays Algebraic Data-types Bit-vectors, Floating points Sequences, Strings

## Basic SAT

  Tie, Shirt = Bools('Tie Shirt')
s = Solver()
s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))
print s.check()
print s.model()

## Basic SMT

I = IntSort()
f = Function('f', I, I)
x, y, z = Ints('x y z')
A = Array('A',I,I)

fml = Implies(x + 2 == y, f(Select(Store(A, x, 3), y - 2)) == f(y - x + 1))

s = Solver()
s.add(Not(fml))
print s.check()

## Logical Language

• Terms
• Logical Connectives
• Quantifiers, Variables

## DPLL [20]

### CDCL: Modern Search [50]

• Efficient indexing (two-watch literal)

• Non-chronological backtracking (backjumping)

• Lemma learning

• Variable and phase selection

• Garbage collection, restarts

### CDCL: State [45]

• : Atomic predicates

• : Literals over atoms

• : Partial assignment without complementary literals.

• : A clause - disjunction of literals.

• : a decision literal.

• : a literal with explanation clause , where is a disjunct in . The literal is assigned relative to partial assignment when all other literals in occur negatively in .

• : A set of clauses.

### Models and Proofs

Theorem 1.
For every , exactly one of the two conditions hold:

• for some where .
• for some where and some resolution proof .

Corollary 1.

CDCL realizes the dichotomy by interleaving model and consequence finding:

Corollary 2.
If , then for every where : .

Corollary 3.
If , i.e., for some , then for every consequence from using forced literals in it is the case that and there is no such that .

### Realizing the dichotomy

Main invariants preserved by CDCL:

• Conflict state: For the state it is the case that and .
• Propagation: For the state and , whenever , then and .

### Illustrating the invariants

if

• Finds First Unique Implication Point (FUIP)
• minimizes number of decision literals in .
• maximizes propagated literals in

## Equality and Uninterpreted functions

### EUF

  (declare-sort A)
(declare-fun f (A) A)
(declare-const x A)
(assert (= (f (f x)) x))
(assert (= (f (f (f x))) x))
(check-sat)

(assert (not (= (f x) x)))
(check-sat)

### Disequalities

Variants of union-find are effective to decide equality.

Congruence rule

### EUF Models

A satisfiable version:

### EUF Models (II)

• Associate a distinct value with each equivalence class.

## Linear Arithmetic

### Linear Arithmetic Example

(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)
(get-model) ; display the model  

### Algorithmic Fragments of Arithmetic

Logic Fragment Solver Example
LRA Linear Real Arithmetic Dual Simplex
LIA Linear Integer Arithmetic CutSat
LIRA Mixed Real/Integer Cuts + Branch
IDL Integer Difference Logic Floyd-Warshall
RDL Real Difference Logic Bellman-Ford
UTVPI Unit two-variable per inequality
NRA Polynomial Real Arithmetic Model based CAD

### Other Fragments of Arithmetic

• NIA - There is no decision procedure for integer polynomial constraints

• Z3 falls back to incomplete heuristics
• NIA over bounded integers may get translated to bit-vector constraints

Theories, where Z3 falls back to general solvers:

• Bi-linear real arithmetic

• Non-unit two-variable per inequality

• At most one unit positive variable per inequality (Horn)

### Bellman-Ford

Solve difference logic using graph Bellman-Ford network flow algorithm. Negative cycle unsat.

### General form Simplex [21]

General form and

Only bounds (e.g., ) are asserted during search.

### From Definitions to a Tableau

- are basic (dependent)
- are non-basic

### Pivoting

• Value of non-basic variable can be chosen between and .
• Value of basic variable is a function of non-basic variable values.
• Pivoting swaps basic and non-basic variables.
• used to get values of basic variables within bounds.

## Arrays

### Arrays

; This example illustrates different uses of the arrays
; supported in Z3.
; This includes Combinatory Array Logic
; (de Moura & Bjorner, FMCAD 2009).
;
(define-sort A () (Array Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun a1 () A)
(declare-fun a2 () A)
(declare-fun a3 () A)
(push) ; illustrate select-store
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
(assert (not (= x y)))
(check-sat)
(pop)
(define-fun all1_array () A ((as const A) 1))
(simplify (select all1_array x))
(define-sort IntSet () (Array Int Bool))
(declare-fun a () IntSet)
(declare-fun b () IntSet)
(declare-fun c () IntSet)
(push) ; illustrate map
(assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a))))))
(check-sat)
(pop)
(push)
(assert (and (select ((_ map and) a b) x) (not (select a x))))
(check-sat)
(pop)
(push)
(assert (and (select ((_ map or) a b) x) (not (select a x))))
(check-sat)
(get-model)
(assert (and (not (select b x))))
(check-sat)
;; unsat, so there is no model.
(pop)
(push) ; illustrate default
(assert (= (default a1) 1))
(assert (not (= a1 ((as const A) 1))))
(check-sat)
(get-model)
(assert (= (default a2) 1))
(assert (not (= a1 a2)))
(check-sat)
(get-model)
(pop)
(exit)    

### Arrays as Combinators [42]

  A = Array(Index, Elem) # array sort

a[i]             # index array 'a' at index 'i'
# Select(a, i)

Store(a, i, v)   # update array 'a' with value 'v' at index 'i'
# = lambda j: If(i == j, v, a[j])

Const(v, A)      # constant array
# = lambda j: v

Map(f, a)        # map function 'f' on values of 'a'
# = lambda j: f(a[j])

Ext(a, b)        # Extensionality
# Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

### Array Decision Procedure

Example Store(a, i, v)

• Each occurrence of Store(a, i, v) and b[j],

• Assert Store(a, i, v)[j] == If(i == j, v, a[j])
• Assert Store(a, i, v)[i] == v
• Each shared occurrences of :

• Assert .
• Suppose we are given a model satisfying all asserted equalities.

• assigns values to terms.
• Extend: .
• Claim: satisfies Store axioms.

### Efficient Array Decision Procedures

• Use current partial interpretation to guide axiom instantiation.

• Rough sketch:

• If (congruent) in current state
• Assert .
• If in current state
• Assert
• Also important to limit set of pairs.

• Z3 uses relevancy propagation to prune don't care literals
• Boolector uses dual propagation to extract small implicant

## Bit-Vectors

### Bit-Vectors

(define-fun is-power-of-two ((x (_ BitVec 4))) Bool
(= #x0 (bvand x (bvsub x #x1))))
(declare-const a (_ BitVec 4))
(assert
(not (= (is-power-of-two a)
(or (= a #x0)
(= a #x1)
(= a #x2)
(= a #x4)
(= a #x8)))))
(check-sat)

## Floating Points

### Floating point example

(declare-fun X () (_ FloatingPoint 11 53))

(assert (fp.isNormal X))
(assert (not (fp.isSubnormal X)))
(assert (not (fp.isZero X)))
(assert (not (fp.isInfinite X)))
(assert (not (fp.isNaN X)))
(assert (not (fp.isNegative X)))
(assert (fp.isPositive X))

(check-sat)
(get-model)

## Sequences and Strings

### Sequence Example

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof b a))
(assert (str.suffixof c a))
(assert (= (str.len a) (+ (str.len b) (str.len c))))
(assert (not (= a (str.++ b c))))
(check-sat)