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

Output.

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

### Configuration

The command set-option is used to configure Z3.

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

• (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.

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.

E.g. check the excluded middle law

Verification with Python API (z3py)

## Uninterpreted functions and constants

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

in Python API

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.

### Division

Support division

E.g. in Python API

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

We get the True.

### Bitvector Arithmetic and Bitwise Operations

and the print

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

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

with Python API

## Arrays

### Select and Store

exercise in Python API

and the output

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.

with Python API

### Scalars

A scalar sort is a finate domain sort.

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

with Python API

### Recursive datatypes

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

like define lst with Python API

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.