Introduction

What is Z3

Z3 is a state-of-art theorem prover from Microsoft Research.

Check sat of logical formulas. Match for software analysis and verification tools.

Low level tool.

Basic Commands

Input format (syntax) is an extension of one defined by the SMT-LIB 2.0 standard.

(help): print the help
(echo <string>): display the given string
(declare-const <symbol> <sort>): declare a constant of a given type (aka sort)
(declare-fun <symbol> (<sort>*) <sort>): declare a function

The command assert adds a formula into the Z3 internal stack. check-sat lets us know if there is an interpretation for all the declared constants and functions that makes all asserted formulas in Z3 stack true.

(assert <term>): assert term
(check-sat <boolean-constants>*): check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true.

When check-sat returns sat(satisfied), the command get-model can be used to retrieve an interpretation. The interpretation is provided using definitions.

(get-model): retrieve model for the last check-sat command
(get-proof): retrieve proof

E.g.

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
(get-model)

Output.

sat
(model
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

Using Scopes

push and pop commands are used for the purpose to share several definitions and assertions. The push and pop commands can optionally receive a numeral argument as specifed by the SMT 2 language.

(push <number>?): push 1 (or ) scopes.
(pop <number>?): pop 1 (or ) scopes.

E.g. (TODO: need to test it).

(declare-const x Int)
(declare-const y Int)
(push) ; push the declarations of x and y
(declare-const z Int)
(push) ; push z
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)
(get-model) ; get the interpretation
(pop) ; remove the two assertions
(pop) ; pop the declaration of z
(push) ; push the declarations of x and y
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 21))
(check-sat) ; not sat
(pop)
(push)
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 4))
(check-sat) ; sat
(get-model) ; get the interpretation

(declare-const p Bool)
(pop)
(assert p) ; error, since declaration of p was removed from the stack

Configuration

The command set-option is used to configure Z3.

But I haven't found the related OCaml API to these configurations. (TODO)

Additional commands

(display) <term>): display the given term(aka expression).
(simplify <term> (<keyword> <value>)*): simplify the expr

From the [z3.mli] we can find the definition of simplify in OCaml.

1
2
3

(** Returns a simplified version of the expression.
      {!get_simplify_help} *)
  val simplify : Expr.expr -> Params.params option -> expr

create a boolean sort

(define-sort [symbol] ([symbol]+) [sort]): define an abbreviation for a sort expression

Maybe map to mk_sort in [z3.mli].

Propositional Logic

So here we meet propositional logic in z3.

Satisfiability and Validity

We need to emphasize the differences between satisfiability and validity.

Satifiability is about finding a solution to a set of constraints.
Validity is about finding a proof of a statement.

In Coq, we always intros to get certain Hypotheses though when we try to prove a proposition with implication , we assumes the Hypotheses are right. So we often want to prove a theorm which notes a proposition is validity.

Back to Z3, consider a formula F with some uninterpreted constants, say a and b. We can ask whether F is valid, that is whether it is always true for any combination of values for a and b. If F is always true, then not F is always false, and then not F will not have any satisfying assignment; that is, not F is unsatisfiable. That is, F is valid precisely when not F is not satisfiable (is unsatisfiable). Alternately, F is satisfiable if and only if not F is not valid (is invalid). Z3 finds satisfying assignments (or report that there are none).

E.g. check the deMorgan's law is valid.

(declare-const a Bool)
(declare-const b Bool)
(define-fun demorgan () Bool
    (= (and a b) (not (or (not a) (not b)))))
(assert (not demorgan))
(check-sat)

E.g. check the excluded middle law

(declare-const a Bool)
(define-fun exmi () Bool
    (or a (not a)
(assert (not exmi))
(check-sat)

Verification with Python API (z3py)

from z3 import *

# create a fresh propositional variable uniquely identified by its name 'p'
slvr = Solver()
p = Bool('p')

# excluded middle
solve(Not(Or(p, Not(p))))

# Pierce's law
q = Bool('q')
solve(Not(Implies(Implies(Implies(p, q), p), p)))

# De Mogan's law
a = Bool('a')
b = Bool('b')
and_a_b = And(a,b)
not_or = Not( Or (Not(a),Not(b)))
solve(eq(and_a_b,not_or))

Uninterpreted functions and constants

Constants are just functions that take no arguments. So everything is really just a function.

(declare-fun f (Int) Int)
(declare-fun a () Int) ; a is a constant
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
(assert (> a 20))
(assert (> b a))
(assert (= (f 10) 1))
(check-sat)
(get-model)

in Python API

slvr = Solver()
A = DeclareSort('A')
x = Const('x', A)
y = Const('y', A)
f = Function('f', A, A)  # f : a -> a
slvr.add(f(f(x)) == x)
slvr.add(f(x) == y )
slvr.add(Not( x == y))
print (slvr)
print (slvr.check())
print (slvr.model())

The notation of A!val!0 means \(A_{val_0}\)

Arithmetic

Builtin support for integer and real constants. These two types (sorts) represent the mathematical integers and reals.

Not convert automatically integers into reals and vice-versa.

Nonlinear arithmetic

Nonlinear arithmetic is undecidable. Note that, this does not prevent Z3 from returning an answer for many nonlinear problems. The real limit is that there will always be a nonlinear integer arithmetic formula that it will fail produce an answer.

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat) ; return unknown for nonlinear real arithmetic

(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)

(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

Division

Support division

E.g. in Python API

a = Int('a')
# r1  = Int('r1')
# r2 = Int('r2')
# r3 = Int('r3')
# r4 = Int('r4')
r = [Int('r' + str(i)) for i in range(0, 10)]
slvr.add(a == 10, r[1] == a/4, r[2] == a % 4)
slvr.add(r[3] == a % 4, r[4] == a / -4)
slvr.add(r[5] == a % -4, r[6] == a % -4)
print (slvr.check())

Bitvectors

(_ bv20 8): a bitvector of size 8 that representes the numeral 20. Desplay as #x14
(_ bv10 32): a bitvector of size 32 that representes the numeral 10. Desplay as #x0000000a (a single num in hexadecimal format represent size 4).

By default, Z3 display bitvectors in hexadecimal format if the bitvector size is a multiple of 4, and in binary otherwise.

In Python API the function BitVecVal(10,32) creates a bit-vector of size 32 containing the value 10.

1
2
3

a = BitVecVal(-1,16)
b = BitVecVal(65535,16)
print(simplify(a==b))

We get the True.

Bitvector Arithmetic and Bitwise Operations

(simplify (bvadd #x07 #x03)) ; addition
(simplify (bvsub #x07 #x03)) ; subtraction
(simplify (bvneg #x07)) ; unary minus
(simplify (bvmul #x07 #x03)) ; multiplication
(simplify (bvurem #x07 #x03)) ; unsigned remainder
(simplify (bvsrem #x07 #x03)) ; signed remainder
(simplify (bvsmod #x07 #x03)) ; signed modulo
(simplify (bvshl #x07 #x03)) ; shift left
(simplify (bvlshr #xf0 #x03)) ; unsigned (logical) shift right
(simplify (bvashr #xf0 #x03)) ; signed (arithmetical) shift right

and the print

#x0a
#x04
#xf9 ; every bit 1->0 0->1 and bitadd 1
#x15
#x01
#x01
#x01
#x38
#x1e
#xfe

Prove a bitwise version of deMorgan's law in Python API.

# Prove a bitwise version of deMorgan's law:
slvr.pop()
slvr.push()
x = BitVec('x', 64)
y = BitVec('y', 64)
slvr.add(Not(( (~x) & (~y)) == ~(x | y)))
print(slvr)
print(slvr.check())
# we get an unsat
# print(slvr.model())

A common trick

There is a fast way to check that fixed size numbers are powers of two.

A bit-vector x is a power of two or zero if and only if x & (x - 1) is zero.

(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)

with Python API

def power_of_two(x):
    bv_and = x & (x - bv_const_one)
    return bv_and == bv_const_zero


# Bit tricks
x = BitVec('x', 32)
powers = [2**i for i in range(32)]
# fast = And(x != 0, x & (x - 1) == 0)
fast = And(x != bv_const_zero, power_of_two(x))
# fast = power_of_two(x)
slow = Or([x == p for p in powers])
print(fast)
prove(fast == slow)

print("trying to prove buggy version...")
fast = x & (x - 1) == 0
print(fast)
prove(fast == slow)

Arrays

Select and Store

exercise in Python API

def util_print(s: Solver):
    r = s.check()
    print(r)
    if r.__repr__() == "sat":
        print(s.model())


slvr.push()
x = Int('x')
y = Int('y')
a1 = Array('a1', IntSort(), IntSort())
slvr.push()
a2 = Array('a2', IntSort(), IntSort())
util_print(slvr)

slvr.pop()
slvr.add(Select(a1, x) == x)
slvr.add(Store(a1, x, y) == a1)
util_print(slvr)
slvr.add(x != y)
util_print(slvr)
slvr.pop()

and the output

sat
[]
sat
[y = 1, a1 = Store(K(Int, 0), 1, 1), x = 1]
unsat

We can get an array which maps all indices to fixed value using the const construct in Z3. E.g. (as const (Array T1 T2))

Map functions on arrays using map keyword.

Datatypes

Records

A record is specified as a datatype with a single constructor and as many arguments as record elements.

1	`(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))`

with Python API

Pair = Datatype('Pair')
Pair.declare('mk_pair', ('pair_first', IntSort()), ('pair_second', IntSort())) # single constructor
Pair = Pair.create()
mp = Pair.mk_pair
fi = Pair.pair_first
se = Pair.pair_second
p1 = Const('p1', Pair)
p2 = Const('p2', Pair)
slvr.add(p1 == p2)
slvr.add(se(p2) > 20)
util_print(slvr)
slvr.add(fi(p1) != fi(p2))
util_print(slvr)

Scalars

A scalar sort is a finate domain sort.

1	`(declare-datatypes () ((S A B C)))`

The elements of the finite domain are enumerated as distinct constans.

with Python API

S = Datatype('S')
S.declare('A')
S.declare('B')
S.declare('C')
S = S.create()
x = Const('x', S)
y = Const('y', S)
z = Const('z', S)
u = Const('u', S)
slvr.add(Distinct(x, y, z))
util_print(slvr)
slvr.add(Distinct(x, y, z, u))
util_print(slvr)

Recursive datatypes

A recursive datatype declaration includes itself directly (or indirectly) as a component.

like define lst with Python API

slvr.pop()
slvr.push()
Lst = Datatype('Lst')
Lst.declare('nil')
Lst.declare('cons', ('hd', IntSort()), ('tl', Lst))
Lst = Lst.create()
print(Lst.cons(10, Lst.nil).sort())

Z3 will not prove inductive facts. The ground decision procedures for recursive datatypes don't lift to establing inductive facts. Z3 does not contain methods for producing proofs by induction. E.g. therom on all natural numbers.

Quantifiers

Apart from quantifier-free theories (Here Z3 is a decision procedure), Z3 also accepts and can work with formulas that use quantifiers. It is no longer a decision procedure for such formulas in general (and for good reasons, as there can be no decision procedure for first-order logic).

Several approaches to handle quantifiers: patter-based quantifier(effective, inherently incomplete), saturation theorem proving.

Modeling with Quantifiers

Computer Science 形式化验证

形式化验证

本博客所有文章除特别声明外，均采用 CC BY-SA 4.0 协议，转载请注明出处！

专业之外，社区之中上一篇

Coq学习——《Software-Foundation》Volume1.7-IndProp 下一篇

Z3学习——Z3-guide

Introduction

What is Z3

Basic Commands

Using Scopes

Configuration

Additional commands

Propositional Logic

Satisfiability and Validity

Uninterpreted functions and constants

Arithmetic

Nonlinear arithmetic

Division

Bitvectors

Bitvector Arithmetic and Bitwise Operations

A common trick

Arrays

Select and Store

Datatypes

Records

Scalars

Recursive datatypes

Quantifiers

Modeling with Quantifiers