{{ message }}

Instantly share code, notes, and snippets.

# jtpaasch/Z3.quickstart.md

Created Feb 21, 2019
Simple Z3 tutorial

# Z3

## The REPL

In utop:

``````#use "topfind";;
#require "Z3";;
``````

## Integer example

### Contexts

Create a context:

``````let ctx = Z3.mk_context [];;
``````

### Numeral

Create a numeral from the integer `11`:

``````let eleven = Z3.Arithmetic.Integer.mk_numeral_i ctx 11;;
``````

Convert it to a string:

``````Z3.Expr.to_string eleven;;
``````

Alternatively, create a numeral from the string `"11"`:

``````let eleven' = Z3.Arithmetic.Integer.mk_numeral_s ctx "11";;
``````

Convert it to a string:

``````Z3.Expr.to_string eleven';;
``````

### Integer constants

Create a string symbol to represent a variable `x`:

``````let x_symbol = Z3.Symbol.mk_string ctx "x";;
``````

See it as a string:

``````Z3.Symbol.to_string x_symbol;;
``````

Confirm that it's a string symbol:

``````Z3.Symbol.is_string_symbol x_symbol;;
``````

Create an integer constant with the symbol's name:

``````let x = Z3.Arithmetic.Integer.mk_const ctx x_symbol;;
``````

See it as a string:

``````Z3.Exp.to_string x;;
``````

Check the sort:

``````let x_sort = Z3.Expr.get_sort x;;
Z3.Sort.to_string x_sort;;
``````

Alternatively, create the symbol and constant in one shot:

``````let x = Z3.Arithmetic.Integer.mk_const_s ctx "x";;
``````

Another integer constant (e.g., `y`):

``````let y = Z3.Arithmetic.Integer.mk_const_s ctx "y";;
``````

### Boolean expressions

Create the boolean expression `x = 11`:

``````let e1 = Z3.Boolean.mk_eq ctx x eleven;;
``````

Check the sort:

``````let e1_sort = Z3.Expr.get_sort e1;;
Z3.Sort.to_string e1_sort;;
``````

### Solver

Create a solver:

``````let s = Z3.Solver.mk_simple_solver ctx;;
``````

Check if `[x = 11]` is satisfiable:

``````Z3.Solver.check s [e1];;
``````

``````Z3.Solver.add s [e1];;
``````

Then check:

``````Z3.Solver.check s [];;
``````

### Model

Get a model of the solver:

``````let Some m = Z3.Solver.get_model s;;
``````

Convert the model to a string:

``````Z3.Model.to_string m;;
``````

Evaluate an expression in a model:

``````let Some v = Z3.Model.eval m x true;;
``````

Check the value for `x` (it should be `11`):

``````Z3.Expr.to_string v;;
``````

## Bitvector example

### Create a context

Create a context:

``````let ctx = Z3.mk_context [];;
``````

### Bitvector numerals

Create a bitvector numeral 3:

``````let three = Z3.Bitvector.numeral_to_string three;;
``````

### Bitvector sort

Create a bitvector sort for 3-bit words:

``````let w_3bit = Z3.BitVector.mk_sort ctx 3;;
``````

Check the size:

``````Z3.BitVector.get_size w_wbit;;
``````

Print it:

``````Z3.Sort.to_string w_3bit;;
``````

### Bitvector constants

Create a 3-bit wide word constant, called `x`:

``````let x = Z3.BitVector.mk_const_s ctx "x" 3;;
``````

Print the symbol:

``````Z3.Expr.to_string x;;
``````

Confirm that it's sort is a 3-bit bitvector:

``````Z3.Sort.to_string (Z3.Expr.get_sort x);;
``````

### Boolean expressions

Create the boolean expression `x = 0b011`:

``````let e2 = Z3.Boolean.mk_eq ctx x three;;
``````

Check the sort:

``````let e2_sort = Z3.Expr.get_sort e2;;
Z3.Sort.to_string e2_sort;;
``````

### Solver

Create a solver:

``````let s = Z3.Solver.mk_simple_solver ctx;;
``````

Check if `[x = 0b011]` is satisfiable:

``````Z3.Solver.check s [e2];;
``````

### Model

Get a model of the solver:

``````let Some m = Z3.Solver.get_model s;;
``````

Convert the model to a string:

``````Z3.Model.to_string m;;
``````

Evaluate an expression in a model:

``````let Some v = Z3.Model.eval m x true;;
``````

Check the value for `x` (it should be `0b011`):

``````Z3.Expr.to_string v;;
``````