Skip to main content
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:
  1. Read-over-Write (same index): Select(Store(A, i, v), i) = v
  2. Read-over-Write (different index): i ≠ j ⟹ Select(Store(A, i, v), j) = Select(A, j)
  3. 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

Build docs developers (and LLMs) love

Get started for freeTalk to us