C API Reference - Z3 Theorem Prover

The Z3 C API is the foundational interface to Z3. All other language bindings are built on top of it.

Core Types

The Z3 C API uses opaque pointer types for all objects:

Fundamental Types

Z3_config

opaque pointer

Configuration object used to initialize contexts. Set parameters before creating a context.

Z3_context

opaque pointer

Manager of all Z3 objects. Required for all API calls. Stores global configuration and manages memory.

Z3_symbol

opaque pointer

Lisp-like symbol used to name types, constants, and functions. Can be created from strings or integers.

Z3_ast

opaque pointer

Abstract syntax tree node representing terms, formulas, and types. Base type for all expressions.

Z3_sort

opaque pointer

Kind of AST representing types (Int, Real, Bool, etc.).

Z3_func_decl

opaque pointer

Function declaration (symbol with signature).

Z3_app

opaque pointer

Function application (function symbol applied to arguments).

Solver Types

Z3_solver

opaque pointer

Incremental solver for checking satisfiability of formulas.

Z3_model

opaque pointer

Model (satisfying assignment) for satisfiable formulas.

Z3_params

opaque pointer

Parameter set for configuring solvers, tactics, and other components.

Advanced Types

Z3_tactic

opaque pointer

Building block for custom solvers.

Z3_goal

opaque pointer

Set of formulas that can be solved or transformed.

Z3_fixedpoint

opaque pointer

Context for the recursive predicate solver (Datalog engine).

Z3_optimize

opaque pointer

Context for solving optimization queries (maximize/minimize).

Enumerations

Z3_lbool

Lifted Boolean type for satisfiability results:

typedef enum {
    Z3_L_FALSE = -1,  // Formula is unsatisfiable
    Z3_L_UNDEF,       // Result is unknown
    Z3_L_TRUE         // Formula is satisfiable
} Z3_lbool;

Z3_sort_kind

The different kinds of sorts (types):

typedef enum {
    Z3_UNINTERPRETED_SORT,    // Uninterpreted sort
    Z3_BOOL_SORT,             // Boolean
    Z3_INT_SORT,              // Integer
    Z3_REAL_SORT,             // Real
    Z3_BV_SORT,               // Bit-vector
    Z3_ARRAY_SORT,            // Array
    Z3_DATATYPE_SORT,         // Datatype
    Z3_RELATION_SORT,         // Relation
    Z3_FINITE_DOMAIN_SORT,    // Finite domain
    Z3_FLOATING_POINT_SORT,   // Floating-point
    Z3_ROUNDING_MODE_SORT,    // Rounding mode
    Z3_SEQ_SORT,              // Sequence
    Z3_RE_SORT,               // Regular expression
    Z3_CHAR_SORT,             // Character
    Z3_TYPE_VAR,              // Type variable
    Z3_UNKNOWN_SORT = 1000
} Z3_sort_kind;

Context Management

Creating Contexts

Z3_mk_config

function

Z3_config Z3_mk_config(void);

Create a configuration object. Use Z3_set_param_value to set parameters.

Z3_del_config

function

void Z3_del_config(Z3_config c);

Delete configuration object. Call after creating context.

Z3_set_param_value

function

void Z3_set_param_value(Z3_config c, const char *param_id, const char *param_value);

Set a configuration parameter. Common parameters:

"model": "true" to enable model generation
"proof": "true" to enable proof generation
"timeout": milliseconds (e.g., "1000")

Z3_mk_context

function

Z3_context Z3_mk_context(Z3_config c);

Create a context using the given configuration.

Z3_del_context

function

void Z3_del_context(Z3_context c);

Delete context and all associated objects.

Version Information

Z3_get_version

function

void Z3_get_version(unsigned *major, unsigned *minor, unsigned *build, unsigned *revision);

Get Z3 version numbers.

Symbols

Z3_mk_string_symbol

function

Z3_symbol Z3_mk_string_symbol(Z3_context c, const char *s);

Create a symbol from a string.

Z3_mk_int_symbol

function

Z3_symbol Z3_mk_int_symbol(Z3_context c, int i);

Create a symbol from an integer.

Sorts (Types)

Basic Sorts

Z3_mk_bool_sort

function

Z3_sort Z3_mk_bool_sort(Z3_context c);

Create Boolean sort.

Z3_mk_int_sort

function

Z3_sort Z3_mk_int_sort(Z3_context c);

Create integer sort.

Z3_mk_real_sort

function

Z3_sort Z3_mk_real_sort(Z3_context c);

Create real sort.

Z3_mk_bv_sort

function

Z3_sort Z3_mk_bv_sort(Z3_context c, unsigned sz);

Create bit-vector sort of size sz.

Array Sorts

Z3_mk_array_sort

function

Z3_sort Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);

Create array sort (maps from domain to range).

Constants and Variables

Z3_mk_const

function

Z3_ast Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);

Create a constant (0-arity function) with given symbol and type.

Z3_mk_int

function

Z3_ast Z3_mk_int(Z3_context c, int v, Z3_sort ty);

Create an integer numeral.

Z3_mk_real

function

Z3_ast Z3_mk_real(Z3_context c, int num, int den);

Create a real numeral num/den.

Boolean Operations

Z3_mk_true

function

Z3_ast Z3_mk_true(Z3_context c);

Create the true constant.

Z3_mk_false

function

Z3_ast Z3_mk_false(Z3_context c);

Create the false constant.

Z3_mk_not

function

Z3_ast Z3_mk_not(Z3_context c, Z3_ast a);

Create NOT expression.

Z3_mk_and

function

Z3_ast Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create n-ary AND expression.

Z3_mk_or

function

Z3_ast Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create n-ary OR expression.

Z3_mk_implies

function

Z3_ast Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);

Create implication t1 => t2.

Z3_mk_iff

function

Z3_ast Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);

Create bi-implication (equivalence) t1 <=> t2.

Arithmetic Operations

Z3_mk_add

function

Z3_ast Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create n-ary addition.

Z3_mk_sub

function

Z3_ast Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create n-ary subtraction.

Z3_mk_mul

function

Z3_ast Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create n-ary multiplication.

Z3_mk_div

function

Z3_ast Z3_mk_div(Z3_context c, Z3_ast t1, Z3_ast t2);

Create division (real division or integer division).

Z3_mk_mod

function

Z3_ast Z3_mk_mod(Z3_context c, Z3_ast t1, Z3_ast t2);

Create modulo operation.

Comparison Operations

Z3_mk_eq

function

Z3_ast Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);

Create equality l = r.

Z3_mk_distinct

function

Z3_ast Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);

Create distinct constraint (all arguments pairwise different).

Z3_mk_lt

function

Z3_ast Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);

Create less-than t1 < t2.

Z3_mk_le

function

Z3_ast Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);

Create less-than-or-equal t1 <= t2.

Z3_mk_gt

function

Z3_ast Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);

Create greater-than t1 > t2.

Z3_mk_ge

function

Z3_ast Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);

Create greater-than-or-equal t1 >= t2.

Solver API

Creating Solvers

Z3_mk_solver

function

Z3_solver Z3_mk_solver(Z3_context c);

Create a new solver instance.

Z3_solver_inc_ref

function

void Z3_solver_inc_ref(Z3_context c, Z3_solver s);

Increment solver reference count.

Z3_solver_dec_ref

function

void Z3_solver_dec_ref(Z3_context c, Z3_solver s);

Decrement solver reference count.

Adding Constraints

Z3_solver_assert

function

void Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);

Assert constraint to the solver.

Z3_solver_push

function

void Z3_solver_push(Z3_context c, Z3_solver s);

Create a backtracking point (save state).

Z3_solver_pop

function

void Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);

Backtrack n scopes.

Checking Satisfiability

Z3_solver_check

function

Z3_lbool Z3_solver_check(Z3_context c, Z3_solver s);

Check satisfiability of assertions. Returns Z3_L_TRUE, Z3_L_FALSE, or Z3_L_UNDEF.

Z3_solver_check_assumptions

function

Z3_lbool Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
                                     unsigned num_assumptions,
                                     Z3_ast const assumptions[]);

Check satisfiability under given assumptions.

Getting Results

Z3_solver_get_model

function

Z3_model Z3_solver_get_model(Z3_context c, Z3_solver s);

Get model for last satisfiable check. Requires "model" parameter to be "true".

Z3_solver_get_proof

function

Z3_ast Z3_solver_get_proof(Z3_context c, Z3_solver s);

Get proof for last unsatisfiable check. Requires "proof" parameter to be "true".

Z3_solver_get_unsat_core

function

Z3_ast_vector Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);

Get unsat core (subset of assertions that are unsatisfiable).

Model API

Z3_model_inc_ref

function

void Z3_model_inc_ref(Z3_context c, Z3_model m);

Increment model reference count.

Z3_model_dec_ref

function

void Z3_model_dec_ref(Z3_context c, Z3_model m);

Decrement model reference count.

Z3_model_eval

function

Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t,
                      Z3_bool model_completion, Z3_ast *v);

Evaluate expression t in model m. Result stored in v.

String Conversion

Z3_ast_to_string

function

Z3_string Z3_ast_to_string(Z3_context c, Z3_ast a);

Convert AST to string (S-expression format).

Z3_solver_to_string

function

Z3_string Z3_solver_to_string(Z3_context c, Z3_solver s);

Convert solver state to string.

Z3_model_to_string

function

Z3_string Z3_model_to_string(Z3_context c, Z3_model m);

Convert model to string.

SMT-LIB Parsing

Z3_parse_smtlib2_string

function

Z3_ast_vector Z3_parse_smtlib2_string(Z3_context c,
                                      const char *str,
                                      unsigned num_sorts,
                                      Z3_symbol const sort_names[],
                                      Z3_sort const sorts[],
                                      unsigned num_decls,
                                      Z3_symbol const decl_names[],
                                      Z3_func_decl const decls[]);

Parse SMT-LIB2 string with custom sorts and declarations.

Resources

Full C API Documentation

Official Z3 C API reference

C Examples

Complete examples in the Z3 repository

Header File

Browse the z3.h header file

Getting Started

Learn the basics of the C API

Python

C++

C

Java

.NET

JavaScript/TypeScript

Go

OCaml

​Core Types

​Fundamental Types

​Solver Types

​Advanced Types

​Enumerations

​Z3_lbool

​Z3_sort_kind

​Context Management

​Creating Contexts

​Version Information

​Symbols

​Sorts (Types)

​Basic Sorts

​Array Sorts

​Constants and Variables

​Boolean Operations

​Arithmetic Operations

​Comparison Operations

​Solver API

​Creating Solvers

​Adding Constraints

​Checking Satisfiability

​Getting Results

​Model API

​String Conversion

​SMT-LIB Parsing

​Resources

Full C API Documentation

C Examples

Header File

Getting Started

Build docs developers (and LLMs) love

Core Types

Fundamental Types

Solver Types

Advanced Types

Enumerations

Z3_lbool

Z3_sort_kind

Context Management

Creating Contexts

Version Information

Symbols

Sorts (Types)

Basic Sorts

Array Sorts

Constants and Variables

Boolean Operations

Arithmetic Operations

Comparison Operations

Solver API

Creating Solvers

Adding Constraints

Checking Satisfiability

Getting Results

Model API

String Conversion

SMT-LIB Parsing

Resources