Getting Started - Z3 Theorem Prover

The Z3 OCaml bindings provide a functional interface to Z3’s SMT solving capabilities. This guide introduces the core concepts and usage patterns.

Quick Start

Here’s a simple Z3 program in OCaml:

example.ml

open Z3
open Z3.Arithmetic
open Z3.Boolean
open Z3.Solver

let () =
  (* Create context *)
  let ctx = mk_context [] in
  
  (* Create integer variable *)
  let x = Integer.mk_const_s ctx "x" in
  let zero = Integer.mk_numeral_i ctx 0 in
  
  (* Create constraint: x > 0 *)
  let constraint_ = mk_gt ctx x zero in
  
  (* Create solver and add constraint *)
  let solver = mk_solver ctx None in
  Solver.add solver [constraint_];
  
  (* Check satisfiability *)
  match check solver [] with
  | SATISFIABLE ->
      Printf.printf "SAT\n";
      (match get_model solver with
       | Some model ->
           Printf.printf "Model: %s\n" (Model.to_string model)
       | None -> ())
  | UNSATISFIABLE -> Printf.printf "UNSAT\n"
  | UNKNOWN -> Printf.printf "UNKNOWN\n"

Compile and run:

ocamlfind ocamlopt -thread -package z3 -linkpkg example.ml -o example
./example

Core Concepts

Context

All Z3 operations require a context:

let ctx = Z3.mk_context []

With custom configuration:

let ctx = Z3.mk_context [
  ("model", "true");
  ("proof", "false");
  ("timeout", "5000")
]

Module Structure

The Z3 OCaml API is organized into modules:

Z3

Core module with context and basic operations

Z3.Symbol

Symbol creation and manipulation

Z3.Sort

Type/sort operations

Z3.Expr

Expression construction

Z3.Boolean

Boolean logic operations

Z3.Arithmetic

Arithmetic operations

Z3.BitVector

Bit-vector operations

Z3.Solver

Solver interface

Opening Modules

Typical imports:

open Z3                    (* Core API *)
open Z3.Symbol             (* Symbols *)
open Z3.Sort               (* Sorts *)
open Z3.Expr               (* Expressions *)
open Z3.Boolean            (* Boolean logic *)
open Z3.Arithmetic         (* Arithmetic *)
open Z3.Arithmetic.Integer (* Integer arithmetic *)
open Z3.Arithmetic.Real    (* Real arithmetic *)
open Z3.Solver             (* Solver *)

Creating Expressions

Integer Arithmetic

open Z3.Arithmetic.Integer

let ctx = mk_context [] in

(* Variables *)
let x = mk_const_s ctx "x" in
let y = mk_const_s ctx "y" in

(* Constants *)
let zero = mk_numeral_i ctx 0 in
let ten = mk_numeral_i ctx 10 in
let five = mk_numeral_s ctx "5" in

(* Arithmetic operations *)
let sum = mk_add ctx [x; y] in
let diff = mk_sub ctx [x; y] in
let prod = mk_mul ctx [x; y] in

Real Arithmetic

open Z3.Arithmetic.Real

let ctx = mk_context [] in

(* Variables *)
let a = mk_const_s ctx "a" in
let b = mk_const_s ctx "b" in

(* Constants *)
let half = mk_numeral_nd ctx 1 2 in  (* 1/2 *)
let pi_approx = mk_numeral_s ctx "3.14159" in

(* Operations *)
let sum = mk_add ctx [a; b] in

Boolean Logic

open Z3.Boolean

let ctx = mk_context [] in

let p = mk_const_s ctx "p" in
let q = mk_const_s ctx "q" in

(* Logical operations *)
let and_expr = mk_and ctx [p; q] in
let or_expr = mk_or ctx [p; q] in
let not_expr = mk_not ctx p in
let implies = mk_implies ctx p q in
let iff = mk_iff ctx p q in

Comparisons

open Z3.Arithmetic.Integer
open Z3.Boolean

let x = mk_const_s ctx "x" in
let y = mk_const_s ctx "y" in
let zero = mk_numeral_i ctx 0 in

(* Comparisons *)
let eq = mk_eq ctx x y in
let lt = mk_lt ctx x y in
let le = mk_le ctx x y in
let gt = mk_gt ctx x zero in
let ge = mk_ge ctx x zero in

Using the Solver

Basic Solving

open Z3
open Z3.Arithmetic.Integer
open Z3.Boolean
open Z3.Solver

let ctx = mk_context [] in
let x = mk_const_s ctx "x" in
let y = mk_const_s ctx "y" in
let ten = mk_numeral_i ctx 10 in
let two = mk_numeral_i ctx 2 in

(* Create constraints *)
let eq1 = mk_eq ctx (mk_add ctx [x; y]) ten in
let eq2 = mk_eq ctx (mk_sub ctx [x; y]) two in

(* Create solver *)
let solver = mk_solver ctx None in

(* Add constraints *)
Solver.add solver [eq1; eq2];

(* Check and get result *)
match check solver [] with
| SATISFIABLE ->
    Printf.printf "Satisfiable!\n";
    (match get_model solver with
     | Some model ->
         Printf.printf "x = %s\n" 
           (Expr.to_string (Model.eval model x true |> Option.get));
         Printf.printf "y = %s\n"
           (Expr.to_string (Model.eval model y true |> Option.get))
     | None -> ())
| UNSATISFIABLE -> Printf.printf "Unsatisfiable\n"
| UNKNOWN -> Printf.printf "Unknown\n"

Solver with Backtracking

let solver = mk_solver ctx None in

(* Add base constraints *)
Solver.add solver [mk_gt ctx x (mk_numeral_i ctx 0)];

(* Create checkpoint *)
Solver.push solver;

(* Add more constraints *)
Solver.add solver [mk_lt ctx x (mk_numeral_i ctx 10)];
let result1 = check solver [] in  (* x > 0 AND x < 10 *)

(* Backtrack *)
Solver.pop solver 1;

let result2 = check solver [] in  (* Only x > 0 *)

Examples from Source

Example 1: Basic Solver

From examples/ml/ml_example.ml:

let basic_tests (ctx : context) =
  Printf.printf "BasicTests\n";
  
  let fname = mk_string ctx "f" in
  let x = mk_string ctx "x" in
  let y = mk_string ctx "y" in
  let bs = Boolean.mk_sort ctx in
  let domain = [bs; bs] in
  let f = FuncDecl.mk_func_decl ctx fname domain bs in
  
  let fapp = mk_app ctx f [
    Expr.mk_const ctx x bs;
    Expr.mk_const ctx y bs
  ] in
  
  let trivial_eq = mk_eq ctx fapp fapp in
  let goal = mk_goal ctx true false false in
  Goal.add goal [trivial_eq];
  
  let solver = mk_solver ctx None in
  List.iter (fun a -> Solver.add solver [a]) (Goal.get_formulas goal);
  
  if check solver [] != SATISFIABLE then
    raise (TestFailedException "")
  else
    Printf.printf "Test passed.\n"

Example 2: Tactics

Using tactics for preprocessing:

open Z3
open Z3.Tactic
open Z3.Goal

let ctx = mk_context [] in
let x = Arithmetic.Integer.mk_const_s ctx "x" in
let y = Arithmetic.Integer.mk_const_s ctx "y" in

(* Create goal *)
let goal = mk_goal ctx true false false in
Goal.add goal [
  Boolean.mk_gt ctx x (Arithmetic.Integer.mk_numeral_i ctx 10);
  Boolean.mk_eq ctx y (Arithmetic.mk_add ctx [x; 
    Arithmetic.Integer.mk_numeral_i ctx 1])
];

(* Apply simplification tactic *)
let tactic = mk_tactic ctx "simplify" in
let result = Tactic.apply tactic goal None in

Printf.printf "Simplified goals: %d\n" 
  (ApplyResult.get_num_subgoals result);

for i = 0 to ApplyResult.get_num_subgoals result - 1 do
  let subgoal = ApplyResult.get_subgoal result i in
  Printf.printf "Subgoal %d: %s\n" i (Goal.to_string subgoal)
done

Example 3: Model Converter

From examples/ml/ml_example.ml:

let model_converter_test (ctx : context) =
  Printf.printf "ModelConverterTest\n";
  
  let xr = Expr.mk_const ctx (Symbol.mk_string ctx "x") 
                              (Real.mk_sort ctx) in
  let yr = Expr.mk_const ctx (Symbol.mk_string ctx "y") 
                              (Real.mk_sort ctx) in
  
  let g4 = mk_goal ctx true false false in
  Goal.add g4 [mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)];
  Goal.add g4 [mk_eq ctx yr 
    (Arithmetic.mk_add ctx [xr; Real.mk_numeral_nd ctx 1 1])];
  Goal.add g4 [mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)];
  
  (* Apply tactics *)
  let tactic = and_then ctx 
    (mk_tactic ctx "simplify") 
    (mk_tactic ctx "solve-eqs") 
    [] in
  let ar = Tactic.apply tactic g4 None in
  
  (* Solve with results *)
  let solver = mk_solver ctx None in
  List.iter (fun e -> Solver.add solver [e]) 
    (Goal.get_formulas (ApplyResult.get_subgoal ar 0));
  
  let q = check solver [] in
  if q = SATISFIABLE then
    match get_model solver with
    | Some m ->
        Printf.printf "Model: \n%s\n" (Model.to_string m)
    | None -> ()

Working with Models

Evaluating Expressions

let solver = mk_solver ctx None in
Solver.add solver [constraint_];

match check solver [] with
| SATISFIABLE ->
    (match get_model solver with
     | Some model ->
         (* Evaluate with model completion *)
         (match Model.eval model x true with
          | Some value -> Printf.printf "x = %s\n" (Expr.to_string value)
          | None -> Printf.printf "x is unassigned\n");
         
         (* Get all constant interpretations *)
         for i = 0 to Model.get_num_consts model - 1 do
           let decl = Model.get_const_decl model i in
           let interp = Model.get_const_interp model decl in
           match interp with
           | Some v -> 
               Printf.printf "%s = %s\n" 
                 (FuncDecl.get_name decl |> Symbol.to_string)
                 (Expr.to_string v)
           | None -> ()
         done
     | None -> ())
| _ -> ()

Model as String

match get_model solver with
| Some model ->
    Printf.printf "Complete model:\n%s\n" (Model.to_string model)
| None -> ()

Bit-Vectors

open Z3.BitVector

let ctx = mk_context [] in

(* 8-bit variables *)
let x = mk_const_s ctx "x" 8 in
let y = mk_const_s ctx "y" 8 in

(* Constants *)
let ff = mk_numeral ctx "255" 8 in
let zero = mk_numeral ctx "0" 8 in

(* Operations *)
let sum = mk_add ctx x y in
let and_op = mk_and ctx x y in
let shift = mk_shl ctx x y in

(* Comparisons *)
let ult = mk_ult ctx x y in  (* Unsigned less than *)
let slt = mk_slt ctx x y in  (* Signed less than *)

(* Constraints *)
let solver = Solver.mk_solver ctx None in
Solver.add solver [
  Boolean.mk_eq ctx sum ff;
  mk_ugt ctx x y  (* Unsigned greater than *)
];

Arrays

open Z3.Z3Array

let ctx = mk_context [] in
let int_sort = Arithmetic.Integer.mk_sort ctx in

(* Create array sort: Int -> Int *)
let array_sort = mk_sort ctx int_sort int_sort in

(* Create array variable *)
let arr = Expr.mk_const ctx (Symbol.mk_string ctx "arr") array_sort in

(* Array operations *)
let i = Arithmetic.Integer.mk_const_s ctx "i" in
let v = Arithmetic.Integer.mk_numeral_i ctx 42 in

(* Read: arr[i] *)
let read = mk_select ctx arr i in

(* Write: arr[i := 42] *)
let arr2 = mk_store ctx arr i v in

(* Constant array *)
let const_arr = mk_const_array ctx int_sort v in

Quantifiers

open Z3.Quantifier

let ctx = mk_context [] in
let int_sort = Arithmetic.Integer.mk_sort ctx in

(* Create bound variable *)
let x_symbol = Symbol.mk_string ctx "x" in
let x = Expr.mk_bound ctx 0 int_sort in

(* Forall x. x >= 0 => x + 1 > 0 *)
let body = Boolean.mk_implies ctx
  (Boolean.mk_ge ctx x (Arithmetic.Integer.mk_numeral_i ctx 0))
  (Boolean.mk_gt ctx 
    (Arithmetic.mk_add ctx [x; Arithmetic.Integer.mk_numeral_i ctx 1])
    (Arithmetic.Integer.mk_numeral_i ctx 0)) in

let forall = expr_of_quantifier (mk_forall_const ctx
  [Expr.mk_const ctx x_symbol int_sort]
  body
  None [] [] None None) in

Configuration and Parameters

Context Configuration

let ctx = mk_context [
  ("model", "true");           (* Generate models *)
  ("proof", "true");           (* Generate proofs *)
  ("timeout", "10000");        (* 10 second timeout *)
  ("well_sorted_check", "true") (* Type checking *)
]

Solver Parameters

let params = Params.mk_params ctx in
Params.add_bool params (Symbol.mk_string ctx "mbqi") false;
Params.add_int params (Symbol.mk_string ctx "timeout") 5000;

let solver = mk_solver ctx None in
Solver.set_parameters solver params;

Error Handling

try
  let ctx = mk_context [] in
  (* Z3 operations *)
  ()
with
| Z3.Error msg -> 
    Printf.eprintf "Z3 error: %s\n" msg
| e -> 
    Printf.eprintf "Error: %s\n" (Printexc.to_string e)

Statistics

let solver = mk_solver ctx None in
Solver.add solver [constraint_];
let _ = check solver [] in

let stats = Solver.get_statistics solver in
Printf.printf "Statistics:\n%s\n" (Statistics.to_string stats);

(* Access specific statistics *)
for i = 0 to Statistics.get_size stats - 1 do
  let key = Statistics.get_key stats i in
  if Statistics.is_uint stats i then
    Printf.printf "%s: %d\n" key (Statistics.get_uint stats i)
  else if Statistics.is_double stats i then
    Printf.printf "%s: %f\n" key (Statistics.get_double stats i)
done

Version Information

open Z3.Version

let () =
  Printf.printf "Z3 version: %s\n" to_string;
  Printf.printf "Major: %d, Minor: %d, Build: %d, Revision: %d\n"
    major minor build_number revision

Best Practices

Pattern Matching

Use pattern matching for solver results:

match check solver [] with
| SATISFIABLE -> (* handle sat *)
| UNSATISFIABLE -> (* handle unsat *)
| UNKNOWN -> (* handle unknown *)

Option Handling

Many functions return option types:

match Model.eval model expr true with
| Some value -> (* use value *)
| None -> (* handle unassigned *)

List Operations

Z3 often uses lists for multiple arguments:

mk_and ctx [p; q; r]
mk_add ctx [x; y; z]

Module Organization

Import specific modules to avoid namespace pollution:

open Z3.Arithmetic.Integer
(* Not: open Z3.Arithmetic *)

Memory Management

The OCaml bindings handle memory management automatically through OCaml’s garbage collector. You don’t need to manually manage Z3 object lifetimes.

Thread Safety

Z3 contexts are not thread-safe. Use separate contexts in different threads or implement proper synchronization.

Next Steps

API Documentation

Complete OCaml API reference

Examples

More example programs

Z3 Guide

In-depth Z3 tutorial

Source Code

OCaml bindings source

​Quick Start

​Core Concepts

​Context

​Module Structure

Z3

Z3.Symbol

Z3.Sort

Z3.Expr

Z3.Boolean

Z3.Arithmetic

Z3.BitVector

Z3.Solver

​Opening Modules

​Creating Expressions

​Integer Arithmetic

​Real Arithmetic

​Boolean Logic

​Comparisons

​Using the Solver

​Basic Solving

​Solver with Backtracking

​Examples from Source

​Example 1: Basic Solver

​Example 2: Tactics

​Example 3: Model Converter

​Working with Models

​Evaluating Expressions

​Model as String

​Bit-Vectors

​Arrays

​Quantifiers

​Configuration and Parameters

​Context Configuration

​Solver Parameters

​Error Handling

​Statistics

​Version Information

​Best Practices

Pattern Matching

Option Handling

List Operations

Module Organization

​Memory Management

​Thread Safety

​Next Steps

API Documentation

Examples

Z3 Guide

Source Code

Quick Start

Core Concepts

Context

Module Structure

Opening Modules

Creating Expressions

Integer Arithmetic

Real Arithmetic

Boolean Logic

Comparisons

Using the Solver

Basic Solving

Solver with Backtracking

Examples from Source

Example 1: Basic Solver

Example 2: Tactics

Example 3: Model Converter

Working with Models

Evaluating Expressions

Model as String

Bit-Vectors

Arrays

Quantifiers

Configuration and Parameters

Context Configuration

Solver Parameters

Error Handling

Statistics

Version Information

Best Practices

Memory Management

Thread Safety

Next Steps