C API Reference

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

opaque pointer

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

opaque pointer

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

opaque pointer

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

opaque pointer

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

opaque pointer

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

opaque pointer

Function declaration (symbol with signature).

opaque pointer

Function application (function symbol applied to arguments).

Solver Types

opaque pointer

Incremental solver for checking satisfiability of formulas.

opaque pointer

Model (satisfying assignment) for satisfiable formulas.

opaque pointer

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

Advanced Types

opaque pointer

Building block for custom solvers.

opaque pointer

Set of formulas that can be solved or transformed.

opaque pointer

Context for the recursive predicate solver (Datalog engine).

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

function

Z3_config Z3_mk_config(void);

Create a configuration object. Use Z3_set_param_value to set parameters.

function

void Z3_del_config(Z3_config c);

Delete configuration object. Call after creating context.

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")

function

Z3_context Z3_mk_context(Z3_config c);

Create a context using the given configuration.

function

void Z3_del_context(Z3_context c);

Delete context and all associated objects.

Version Information

function

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

Get Z3 version numbers.

Symbols

function

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

Create a symbol from a string.

function

Z3_symbol Z3_mk_int_symbol(Z3_context c, int i);

Create a symbol from an integer.

Sorts (Types)

Basic Sorts

function

Z3_sort Z3_mk_bool_sort(Z3_context c);

Create Boolean sort.

function

Z3_sort Z3_mk_int_sort(Z3_context c);

Create integer sort.

function

Z3_sort Z3_mk_real_sort(Z3_context c);

Create real sort.

function

Z3_sort Z3_mk_bv_sort(Z3_context c, unsigned sz);

Create bit-vector sort of size sz.

Array Sorts

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

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.

function

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

Create an integer numeral.

function

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

Create a real numeral num/den.

Boolean Operations

function

Z3_ast Z3_mk_true(Z3_context c);

Create the true constant.

function

Z3_ast Z3_mk_false(Z3_context c);

Create the false constant.

function

Z3_ast Z3_mk_not(Z3_context c, Z3_ast a);

Create NOT expression.

function

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

Create n-ary AND expression.

function

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

Create n-ary OR expression.

function

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

Create implication t1 => t2.

function

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

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

Arithmetic Operations

function

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

Create n-ary addition.

function

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

Create n-ary subtraction.

function

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

Create n-ary multiplication.

function

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

Create division (real division or integer division).

function

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

Create modulo operation.

Comparison Operations

function

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

Create equality l = r.

function

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

Create distinct constraint (all arguments pairwise different).

function

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

Create less-than t1 < t2.

function

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

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

function

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

Create greater-than t1 > t2.

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

function

Z3_solver Z3_mk_solver(Z3_context c);

Create a new solver instance.

function

void Z3_solver_inc_ref(Z3_context c, Z3_solver s);

Increment solver reference count.

function

void Z3_solver_dec_ref(Z3_context c, Z3_solver s);

Decrement solver reference count.

Adding Constraints

function

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

Assert constraint to the solver.

function

void Z3_solver_push(Z3_context c, Z3_solver s);

Create a backtracking point (save state).

function

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

Backtrack n scopes.

Checking Satisfiability

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.

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

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".

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".

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

function

void Z3_model_inc_ref(Z3_context c, Z3_model m);

Increment model reference count.

function

void Z3_model_dec_ref(Z3_context c, Z3_model m);

Decrement model reference count.

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

function

Z3_string Z3_ast_to_string(Z3_context c, Z3_ast a);

Convert AST to string (S-expression format).

function

Z3_string Z3_solver_to_string(Z3_context c, Z3_solver s);

Convert solver state to string.

function

Z3_string Z3_model_to_string(Z3_context c, Z3_model m);

Convert model to string.

SMT-LIB Parsing

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

​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

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