Expression API

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.

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.

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.

Z3_ast

The true constant

Z3_mk_false

Z3_ast Z3_API Z3_mk_false(Z3_context c);

Create the false Boolean constant.

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

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

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

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

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

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

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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;
}

Core API

Theory Solvers

Advanced

Overview

Types

Z3_ast

Z3_app

Z3_ast_kind

Z3_symbol

Symbol Creation

Z3_mk_int_symbol

Z3_mk_string_symbol

Boolean Expressions

Z3_mk_true

Z3_mk_false

Z3_mk_eq

Z3_mk_distinct

Z3_mk_not

Z3_mk_and

Z3_mk_or

Z3_mk_implies

Z3_mk_ite

Constants and Applications

Z3_mk_const

Z3_mk_app

Numeral Creation

Z3_mk_int

Z3_mk_unsigned_int

Z3_mk_int64

Z3_mk_numeral

AST Inspection

Z3_get_ast_kind

Z3_is_app

Z3_to_app

Z3_get_app_decl

Z3_get_app_num_args

Z3_get_app_arg

Complete Example

​Overview

​Types

​Z3_ast

​Z3_app

​Z3_ast_kind

​Z3_symbol

​Symbol Creation

​Z3_mk_int_symbol

​Z3_mk_string_symbol

​Boolean Expressions

​Z3_mk_true

​Z3_mk_false

​Z3_mk_eq

​Z3_mk_distinct

​Z3_mk_not

​Z3_mk_and

​Z3_mk_or

​Z3_mk_implies

​Z3_mk_ite

​Constants and Applications

​Z3_mk_const

​Z3_mk_app

​Numeral Creation

​Z3_mk_int

​Z3_mk_unsigned_int

​Z3_mk_int64

​Z3_mk_numeral

​AST Inspection

​Z3_get_ast_kind

​Z3_is_app

​Z3_to_app

​Z3_get_app_decl

​Z3_get_app_num_args

​Z3_get_app_arg

​Complete Example

Overview

Types

Z3_ast

Z3_app

Z3_ast_kind

Z3_symbol

Symbol Creation

Z3_mk_int_symbol

Z3_mk_string_symbol

Boolean Expressions

Z3_mk_true

Z3_mk_false

Z3_mk_eq

Z3_mk_distinct

Z3_mk_not

Z3_mk_and

Z3_mk_or

Z3_mk_implies

Z3_mk_ite

Constants and Applications

Z3_mk_const

Z3_mk_app

Numeral Creation

Z3_mk_int

Z3_mk_unsigned_int

Z3_mk_int64

Z3_mk_numeral

AST Inspection

Z3_get_ast_kind

Z3_is_app

Z3_to_app

Z3_get_app_decl

Z3_get_app_num_args

Z3_get_app_arg

Complete Example