Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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];;

Alternatively, add the expression first:

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;;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.