Sort API

Overview

The Sort API provides functions for creating and manipulating Z3 sorts (types). Sorts are used to define the domains of constants, variables, and functions.

Types

Z3_sort

A kind of AST used to represent types/sorts in Z3.

Z3_sort_kind

Enumeration of different sort kinds:

Built-in Sorts

Z3_mk_bool_sort

Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);

Create the Boolean type.

Z3_sort

Boolean sort

Description: This type is used to create propositional variables and predicates. Example:

Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
Z3_ast p = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "p"), bool_sort);

Z3_mk_int_sort

Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);

Create the integer type.

Z3_sort

Integer sort

Description: This is mathematical integers (unbounded), not machine integers. For machine integers, use bit-vectors. Example:

Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);

Z3_mk_real_sort

Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);

Create the real number type.

Z3_sort

Real sort

Description: This is mathematical reals, not floating-point numbers. Example:

Z3_sort real_sort = Z3_mk_real_sort(ctx);
Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), real_sort);

Z3_mk_bv_sort

Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);

Create a bit-vector type of given size.

Z3_sort

Bit-vector sort

Description: Bit-vectors can be used to model machine integers and perform bit-level operations. Example:

Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8);   // 8-bit vector
Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32); // 32-bit vector
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), bv32);

Z3_mk_finite_domain_sort

Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);

Create a named finite domain sort.

Z3_sort

Finite domain sort

Description: To create constants in this domain, use numeric constants from 0 to size-1.

Uninterpreted Sorts

Z3_mk_uninterpreted_sort

Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);

Create a free (uninterpreted) type using the given name.

Z3_sort

Uninterpreted sort

Description: Two free types are considered the same if and only if they have the same name. Example:

Z3_sort Color = Z3_mk_uninterpreted_sort(ctx, Z3_mk_string_symbol(ctx, "Color"));
Z3_ast red = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "red"), Color);
Z3_ast blue = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "blue"), Color);

Z3_mk_type_variable

Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s);

Create a type variable.

Z3_sort

Type variable

Description: Functions using type variables can be applied to instantiations that match the signature.

Composite Sorts

Z3_mk_array_sort

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

Create an array type [domain -> range].

Z3_sort

Array sort

Description: Arrays are commonly used to model heap/memory in software verification. Example:

Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
Z3_ast arr = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "arr"), array_sort);

Z3_mk_tuple_sort

Z3_sort Z3_API Z3_mk_tuple_sort(
    Z3_context c,
    Z3_symbol mk_tuple_name,
    unsigned num_fields,
    Z3_symbol const field_names[],
    Z3_sort const field_sorts[],
    Z3_func_decl* mk_tuple_decl,
    Z3_func_decl proj_decl[]
);

Create a tuple sort.

Z3_sort

Tuple sort

Example:

Z3_symbol field_names[2] = {
    Z3_mk_string_symbol(ctx, "x"),
    Z3_mk_string_symbol(ctx, "y")
};
Z3_sort field_sorts[2] = {
    Z3_mk_int_sort(ctx),
    Z3_mk_int_sort(ctx)
};
Z3_func_decl mk_tuple;
Z3_func_decl proj[2];

Z3_sort point = Z3_mk_tuple_sort(
    ctx,
    Z3_mk_string_symbol(ctx, "mk_point"),
    2,
    field_names,
    field_sorts,
    &mk_tuple,
    proj
);

Z3_mk_seq_sort

Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);

Create a sequence sort.

Z3_sort

Sequence sort

Example:

Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort int_seq = Z3_mk_seq_sort(ctx, int_sort);

Z3_mk_re_sort

Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);

Create a regular expression sort.

Z3_sort

Regular expression sort

Floating-Point Sorts

Z3_mk_fpa_sort

Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);

Create a floating-point sort.

Z3_sort

Floating-point sort

Example:

Z3_sort float32 = Z3_mk_fpa_sort(ctx, 8, 24);  // IEEE 754 single precision
Z3_sort float64 = Z3_mk_fpa_sort(ctx, 11, 53); // IEEE 754 double precision

Z3_mk_fpa_sort_16

Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);

Create the half-precision (16-bit) floating-point sort.

Z3_sort

16-bit float sort

Z3_mk_fpa_sort_32

Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);

Create the single-precision (32-bit) floating-point sort.

Z3_sort

32-bit float sort

Z3_mk_fpa_sort_64

Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);

Create the double-precision (64-bit) floating-point sort.

Z3_sort

64-bit float sort

Z3_mk_fpa_sort_128

Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);

Create the quadruple-precision (128-bit) floating-point sort.

Z3_sort

128-bit float sort

Sort Inspection

Z3_get_sort_kind

Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);

Return the sort kind.

Z3_sort_kind

Sort kind

Z3_get_sort

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);

Return the sort of an AST node.

Z3_sort

Sort of the expression

Z3_get_bv_sort_size

unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);

Return the size of the given bit-vector sort.

unsigned

Size in bits

Z3_get_array_sort_domain

Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);

Return the domain sort of an array sort.

Z3_sort

Domain sort

Z3_get_array_sort_range

Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);

Return the range sort of an array sort.

Z3_sort

Range sort

Sort Conversion

Z3_sort_to_ast

Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);

Convert a sort into an AST node.

Z3_ast

AST representation of sort

Description: Allows using sorts in places that expect AST nodes (e.g., for reference counting).

Complete Example

#include <z3.h>
#include <stdio.h>

int main() {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    
    // Create basic sorts
    Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
    Z3_sort int_sort = Z3_mk_int_sort(ctx);
    Z3_sort bv32_sort = Z3_mk_bv_sort(ctx, 32);
    
    // Create array sort: Int -> Int
    Z3_sort array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
    
    // Create uninterpreted sort
    Z3_sort person_sort = Z3_mk_uninterpreted_sort(
        ctx, 
        Z3_mk_string_symbol(ctx, "Person")
    );
    
    // Inspect sorts
    printf("BV size: %u\n", Z3_get_bv_sort_size(ctx, bv32_sort));
    
    Z3_del_context(ctx);
    return 0;
}

Core API

Theory Solvers

Advanced

Overview

Types

Z3_sort

Z3_sort_kind

Built-in Sorts

Z3_mk_bool_sort

Z3_mk_int_sort

Z3_mk_real_sort

Z3_mk_bv_sort

Z3_mk_finite_domain_sort

Uninterpreted Sorts

Z3_mk_uninterpreted_sort

Z3_mk_type_variable

Composite Sorts

Z3_mk_array_sort

Z3_mk_tuple_sort

Z3_mk_seq_sort

Z3_mk_re_sort

Floating-Point Sorts

Z3_mk_fpa_sort

Z3_mk_fpa_sort_16

Z3_mk_fpa_sort_32

Z3_mk_fpa_sort_64

Z3_mk_fpa_sort_128

Sort Inspection

Z3_get_sort_kind

Z3_get_sort

Z3_get_bv_sort_size

Z3_get_array_sort_domain

Z3_get_array_sort_range

Sort Conversion

Z3_sort_to_ast

Complete Example

​Overview

​Types

​Z3_sort

​Z3_sort_kind

​Built-in Sorts

​Z3_mk_bool_sort

​Z3_mk_int_sort

​Z3_mk_real_sort

​Z3_mk_bv_sort

​Z3_mk_finite_domain_sort

​Uninterpreted Sorts

​Z3_mk_uninterpreted_sort

​Z3_mk_type_variable

​Composite Sorts

​Z3_mk_array_sort

​Z3_mk_tuple_sort

​Z3_mk_seq_sort

​Z3_mk_re_sort

​Floating-Point Sorts

​Z3_mk_fpa_sort

​Z3_mk_fpa_sort_16

​Z3_mk_fpa_sort_32

​Z3_mk_fpa_sort_64

​Z3_mk_fpa_sort_128

​Sort Inspection

​Z3_get_sort_kind

​Z3_get_sort

​Z3_get_bv_sort_size

​Z3_get_array_sort_domain

​Z3_get_array_sort_range

​Sort Conversion

​Z3_sort_to_ast

​Complete Example

Overview

Types

Z3_sort

Z3_sort_kind

Built-in Sorts

Z3_mk_bool_sort

Z3_mk_int_sort

Z3_mk_real_sort

Z3_mk_bv_sort

Z3_mk_finite_domain_sort

Uninterpreted Sorts

Z3_mk_uninterpreted_sort

Z3_mk_type_variable

Composite Sorts

Z3_mk_array_sort

Z3_mk_tuple_sort

Z3_mk_seq_sort

Z3_mk_re_sort

Floating-Point Sorts

Z3_mk_fpa_sort

Z3_mk_fpa_sort_16

Z3_mk_fpa_sort_32

Z3_mk_fpa_sort_64

Z3_mk_fpa_sort_128

Sort Inspection

Z3_get_sort_kind

Z3_get_sort

Z3_get_bv_sort_size

Z3_get_array_sort_domain

Z3_get_array_sort_range

Sort Conversion

Z3_sort_to_ast

Complete Example