Skip to main content

​
Overview

The Expression API provides functions for creating and manipulating Z3 abstract syntax trees (ASTs), which represent terms, formulas, and types.

​
Types

​
Z3_ast

Abstract syntax tree node - the fundamental data structure in Z3 for representing terms, formulas, and types.

​
Z3_app

A kind of AST used to represent function applications. Subtype of Z3_ast.

​
Z3_ast_kind

The different kinds of Z3 AST nodes:

​
Z3_symbol

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

​
Symbol Creation

​
Z3_mk_int_symbol

Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
Create a Z3 symbol using an integer.
​
return
Z3_symbol
New symbol

​
Z3_mk_string_symbol

Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
Create a Z3 symbol using a C string.
​
return
Z3_symbol
New symbol
Example: 
Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
Z3_symbol y_sym = Z3_mk_string_symbol(ctx, "y");

​
Boolean Expressions

​
Z3_mk_true

Z3_ast Z3_API Z3_mk_true(Z3_context c);
Create the true Boolean constant.
​
return
Z3_ast
The true constant

​
Z3_mk_false

Z3_ast Z3_API Z3_mk_false(Z3_context c);
Create the false Boolean constant.
​
return
Z3_ast
The false constant

​
Z3_mk_eq

Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
Create an equality expression (l = r).
​
return
Z3_ast
Equality expression
Example: 
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), Z3_mk_int_sort(ctx));
Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), Z3_mk_int_sort(ctx));
Z3_ast eq = Z3_mk_eq(ctx, x, y); // x = y

​
Z3_mk_distinct

Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
Create an n-ary distinct predicate (all arguments are pairwise distinct).
​
return
Z3_ast
Distinct predicate

​
Z3_mk_not

Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
Create a negation (not a).
​
return
Z3_ast
Negated expression

​
Z3_mk_and

Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
Create an n-ary conjunction (and).
​
return
Z3_ast
Conjunction
Example: 
Z3_ast args[3] = {p, q, r};
Z3_ast conjunction = Z3_mk_and(ctx, 3, args); // p ∧ q ∧ r

​
Z3_mk_or

Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
Create an n-ary disjunction (or).
​
return
Z3_ast
Disjunction

​
Z3_mk_implies

Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
Create an implication (t1 implies t2).
​
return
Z3_ast
Implication

​
Z3_mk_ite

Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
Create an if-then-else expression.
​
return
Z3_ast
If-then-else expression
Example: 
Z3_ast result = Z3_mk_ite(ctx, condition, then_val, else_val);
// if condition then then_val else else_val

​
Constants and Applications

​
Z3_mk_const

Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
Create a constant (0-arity function application).
​
return
Z3_ast
Constant expression
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_app

Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[]);
Create a function application.
​
return
Z3_ast
Function application

​
Numeral Creation

​
Z3_mk_int

Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
Create a numeral of a given sort from an integer.
​
return
Z3_ast
Numeral expression
Example: 
Z3_ast five = Z3_mk_int(ctx, 5, Z3_mk_int_sort(ctx));

​
Z3_mk_unsigned_int

Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
Create a numeral from an unsigned integer.
​
return
Z3_ast
Numeral expression

​
Z3_mk_int64

Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);
Create a numeral from a 64-bit integer.
​
return
Z3_ast
Numeral expression

​
Z3_mk_numeral

Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
Create a numeral from a string representation.
​
return
Z3_ast
Numeral expression
Example: 
Z3_ast large_num = Z3_mk_numeral(ctx, "123456789012345", Z3_mk_int_sort(ctx));
Z3_ast pi_approx = Z3_mk_numeral(ctx, "3.14159", Z3_mk_real_sort(ctx));

​
AST Inspection

​
Z3_get_ast_kind

Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
Return the kind of the given AST.
​
return
Z3_ast_kind
Kind of AST node

​
Z3_is_app

bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
Return true if the given AST is an application.
​
return
bool
True if application, false otherwise

​
Z3_to_app

Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
Convert an AST to an application.
​
return
Z3_app
Application

​
Z3_get_app_decl

Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
Return the declaration of a function application.
​
return
Z3_func_decl
Function declaration

​
Z3_get_app_num_args

unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
Return the number of arguments of a function application.
​
return
unsigned
Number of arguments

​
Z3_get_app_arg

Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
Return the i-th argument of a function application.
​
return
Z3_ast
i-th argument

​
Complete Example

#include <z3.h>

int main() {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    
    // Create integer sort
    Z3_sort int_sort = Z3_mk_int_sort(ctx);
    
    // Create variables x and y
    Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
    Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), int_sort);
    
    // Create expression: x + y = 10
    Z3_ast args[2] = {x, y};
    Z3_ast sum = Z3_mk_add(ctx, 2, args);
    Z3_ast ten = Z3_mk_int(ctx, 10, int_sort);
    Z3_ast constraint = Z3_mk_eq(ctx, sum, ten);
    
    Z3_del_context(ctx);
    return 0;
}

Build docs developers (and LLMs) love

Get started for freeTalk to us