Skip to main content

​
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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].
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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;
}

Build docs developers (and LLMs) love

Get started for freeTalk to us