In utop:
#use "topfind";;
#require "Z3";;
Create a context:
let ctx = Z3.mk_context [];;
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';;
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";;
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;;
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 [];;
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;;
Create a context:
let ctx = Z3.mk_context [];;
Create a bitvector numeral 3:
let three = Z3.Bitvector.numeral_to_string three;;
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;;
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);;
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;;
Create a solver:
let s = Z3.Solver.mk_simple_solver ctx;;
Check if [x = 0b011] is satisfiable:
Z3.Solver.check s [e2];;
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;;