Array Theory

The array theory in Z3 provides reasoning about arrays with arbitrary index and element types. Arrays follow the theory of extensionality: two arrays are equal if they have the same values at all indices.

Array Sorts

Create an array sort with index and element types:

from z3 import *

# Array from integers to integers
A = Array('A', IntSort(), IntSort())

# Array from bit-vectors to booleans
B = Array('B', BitVecSort(32), BoolSort())

# Array from strings to reals
C = Array('C', StringSort(), RealSort())

C API: Z3_mk_array_sort(c, domain, range) (api_array.cpp:26)

Multi-Dimensional Arrays

Create arrays with multiple indices:

# 2D array: Array[Int, Int, Int]
Matrix = Array('Matrix', IntSort(), IntSort(), IntSort())

# 3D array
Tensor = Array('Tensor', IntSort(), IntSort(), IntSort(), RealSort())

C API: Z3_mk_array_sort_n(c, n, domain, range) (api_array.cpp:37)

Basic Operations

Select

Read a value from an array at a given index:

A = Array('A', IntSort(), IntSort())
x = Int('x')

# Read value at index 5
val = A[5]
# Or using Select explicitly
val = Select(A, 5)

solve(A[5] == 10, A[5] == x)
# [A = [5 -> 10, else -> 0], x = 10]

C API: Z3_mk_select(c, a, i) (api_array.cpp:51) Multi-index: Z3_mk_select_n(c, a, n, idxs) (api_array.cpp:76)

Store

Write a value to an array at a given index:

A = Array('A', IntSort(), IntSort())

# Store 42 at index 5
B = Store(A, 5, 42)
# Or using array notation
B = A[5] = 42  # Not valid Python syntax, use Store

solve(B[5] == 42, B[3] == A[3])
# Store preserves all other values

C API: Z3_mk_store(c, a, i, v) (api_array.cpp:106) Multi-index: Z3_mk_store_n(c, a, n, idxs, v) (api_array.cpp:134)

Array Properties

Extensionality

Arrays are equal if they have the same values at all indices:

A = Array('A', IntSort(), IntSort())
B = Array('B', IntSort(), IntSort())

solve(A == B, A[0] == 1, B[0] == 2)
# unsat - arrays differ at index 0

solve(A == B, ForAll([x], A[x] == B[x]))
# sat - arrays are equal

Default Values

Arrays can have default values for uninitialized indices:

# Create array with default value
A = K(IntSort(), 0)  # All elements are 0

solve(A[5] == 0, A[100] == 0)
# sat

C API: Z3_mk_const_array(c, domain, v) creates array where all elements equal v (api_array.cpp:191)

Array Default Accessor

Get the default value of an array: C API: Z3_mk_array_default(c, array) (api_array.cpp:210)

Advanced Operations

Map

Apply a function to every element of arrays:

A = Array('A', IntSort(), IntSort())
B = Array('B', IntSort(), IntSort())

# Map addition over two arrays
# C = λi. A[i] + B[i]
plus = Function('plus', IntSort(), IntSort(), IntSort())
C = Map(plus, A, B)

C API: Z3_mk_map(c, f, n, args) (api_array.cpp:166)

Array Extensionality

Find an index where two arrays differ:

A = Array('A', IntSort(), IntSort())
B = Array('B', IntSort(), IntSort())

s = Solver()
s.add(A != B)

if s.check() == sat:
    # Get index where arrays differ
    # Use Z3_mk_array_ext in C API
    pass

C API: Z3_mk_array_ext(c, arg1, arg2) returns an index where arrays differ if they’re not equal (api_array.cpp:270)

Set Operations

Z3 implements sets as arrays from elements to booleans:

# Set of integers
S = Set('S', IntSort())
T = Set('T', IntSort())

Empty and Full Sets

# Empty set
empty = EmptySet(IntSort())

# Full set (universal set)
full = FullSet(IntSort())

C API: Z3_mk_empty_set, Z3_mk_full_set (api_array.cpp:247, 256)

Set Membership

S = Set('S', IntSort())
x = Int('x')

solve(IsMember(x, S), x == 5)
# x is in set S

C API: Z3_mk_set_member(c, elem, set) (api_array.cpp:284)

Set Operations

S = Set('S', IntSort())
T = Set('T', IntSort())

# Union
U = Union(S, T)

# Intersection
I = Intersection(S, T)

# Difference
D = SetDifference(S, T)

# Complement
C = SetComplement(S)

# Subset
solve(IsSubset(S, T))

C API:

Z3_mk_set_union (api_array.cpp:265)
Z3_mk_set_intersect (api_array.cpp:266)
Z3_mk_set_difference (api_array.cpp:267)
Z3_mk_set_complement (api_array.cpp:268)
Z3_mk_set_subset (api_array.cpp:269)

Add/Remove Elements

S = Set('S', IntSort())

# Add element
S2 = SetAdd(S, 5)

# Remove element
S3 = SetDel(S, 5)

C API: Z3_mk_set_add, Z3_mk_set_del (api_array.cpp:288, 292)

Complete Examples

Example 1: Array Update Sequence

from z3 import *

A = Array('A', IntSort(), IntSort())

# Sequence of updates
B = Store(A, 1, 10)
C = Store(B, 2, 20)
D = Store(C, 3, 30)

s = Solver()
s.add(D[1] == 10)
s.add(D[2] == 20)
s.add(D[3] == 30)
s.add(D[4] == A[4])  # Index 4 unchanged

print(s.check())  # sat

Example 2: Array Equality

from z3 import *

A = Array('A', IntSort(), IntSort())
B = Array('B', IntSort(), IntSort())

# Two arrays are equal iff they agree at all indices
x = Int('x')

s = Solver()
s.add(ForAll([x], A[x] == B[x]))
s.add(A[0] == 5)

if s.check() == sat:
    m = s.model()
    # B[0] must also be 5
    print(m.evaluate(B[0]))  # 5

Example 3: Sparse Array Initialization

from z3 import *

# Create array with default value 0
A = K(IntSort(), 0)

# Set specific indices
A = Store(A, 10, 100)
A = Store(A, 20, 200)
A = Store(A, 30, 300)

solve(
    A[10] == 100,
    A[15] == 0,    # Default value
    A[20] == 200,
    A[99] == 0     # Default value
)

Example 4: Multi-Dimensional Array

from z3 import *

# 2D matrix: rows and columns
Matrix = Array('Matrix', IntSort(), IntSort(), IntSort())

s = Solver()

# Set Matrix[1][2] = 42
Matrix = Store(Matrix, 1, 2, 42)

# Set Matrix[3][4] = 99
Matrix = Store(Matrix, 3, 4, 99)

s.add(Select(Matrix, 1, 2) == 42)
s.add(Select(Matrix, 3, 4) == 99)

print(s.check())  # sat

Example 5: Set Operations

from z3 import *

S = Set('S', IntSort())
T = Set('T', IntSort())

x, y, z = Ints('x y z')

s = Solver()

# x is in S
s.add(IsMember(x, S))

# y is in T
s.add(IsMember(y, T))

# z is in both S and T (intersection)
s.add(IsMember(z, Intersection(S, T)))

s.add(x == 5)
s.add(y == 10)
s.add(z == 7)

if s.check() == sat:
    m = s.model()
    print(f"x={m[x]}, y={m[y]}, z={m[z]}")
    # S contains at least {5, 7}
    # T contains at least {7, 10}

Example 6: As-Array Construction

Create an array from a function:

from z3 import *

# Define a function
f = Function('f', IntSort(), IntSort())

# Create array from function
# A[i] = f(i) for all i
A = Lambda([x], f(x))

solve(A[5] == 10, f(5) == 10)

C API: Z3_mk_as_array(c, f) (api_array.cpp:272)

Query Functions

Get Array Sort Information

# Check number of indices
# Get domain and range sorts

C API:

Z3_get_array_arity(c, s) - number of indices (api_array.cpp:302)
Z3_get_array_sort_domain(c, t) - domain sort (api_array.cpp:315)
Z3_get_array_sort_domain_n(c, t, idx) - nth domain sort (api_array.cpp:329)
Z3_get_array_sort_range(c, t) - range sort (api_array.cpp:343)

Theory Axioms

The array theory is defined by two key axioms:

Read-over-Write (same index): Select(Store(A, i, v), i) = v
Read-over-Write (different index): i ≠ j ⟹ Select(Store(A, i, v), j) = Select(A, j)
Extensionality: (∀i. Select(A, i) = Select(B, i)) ⟹ A = B

Implementation Notes

Arrays are functional and immutable (Store creates a new array)
The theory is decidable for quantifier-free formulas
Array values are represented symbolically (not stored explicitly)
Efficient for sparse updates and reads
No built-in bounds checking (arrays are infinite)

References

Implementation: src/api/api_array.cpp
Theory plugin: src/ast/array_decl_plugin.h
Solver: src/smt/theory_array.h

Core API

Theory Solvers

Advanced

Array Sorts

Multi-Dimensional Arrays

Basic Operations

Select

Store

Array Properties

Extensionality

Default Values

Array Default Accessor

Advanced Operations

Map

Array Extensionality

Set Operations

Empty and Full Sets

Set Membership

Set Operations

Add/Remove Elements

Complete Examples

Example 1: Array Update Sequence

Example 2: Array Equality

Example 3: Sparse Array Initialization

Example 4: Multi-Dimensional Array

Example 5: Set Operations

Example 6: As-Array Construction

Query Functions

Get Array Sort Information

Theory Axioms

Implementation Notes

References

​Array Sorts

​Multi-Dimensional Arrays

​Basic Operations

​Select

​Store

​Array Properties

​Extensionality

​Default Values

​Array Default Accessor

​Advanced Operations

​Map

​Array Extensionality

​Set Operations

​Empty and Full Sets

​Set Membership

​Set Operations

​Add/Remove Elements

​Complete Examples

​Example 1: Array Update Sequence

​Example 2: Array Equality

​Example 3: Sparse Array Initialization

​Example 4: Multi-Dimensional Array

​Example 5: Set Operations

​Example 6: As-Array Construction

​Query Functions

​Get Array Sort Information

​Theory Axioms

​Implementation Notes

​References

Array Sorts

Multi-Dimensional Arrays

Basic Operations

Select

Store

Array Properties

Extensionality

Default Values

Array Default Accessor

Advanced Operations

Map

Array Extensionality

Set Operations

Empty and Full Sets

Set Membership

Set Operations

Add/Remove Elements

Complete Examples

Example 1: Array Update Sequence

Example 2: Array Equality

Example 3: Sparse Array Initialization

Example 4: Multi-Dimensional Array

Example 5: Set Operations

Example 6: As-Array Construction

Query Functions

Get Array Sort Information

Theory Axioms

Implementation Notes

References