Z3 SMT Solver¶

Z3 is a high-performance Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Clausal's Z3 integration exposes Z3's multi-theory solver as constraint predicates under the z3.* module namespace.

Unlike Clausal's native constraint solvers (CLP(Z), CLP(R), CLP(Q), CLP(B)), which each handle one domain, Z3 handles integers, reals, booleans, bitvectors, arrays, sets, strings, and uninterpreted functions in a single solver. Constraints from different theories can coexist on the same trail and Z3 handles the theory combination internally.

The implementation lives in clausal/logic/clpz3.py.

Note

Requires z3-solver: pip install z3-solver

Constraint Blocks¶

Constraints are posted via theory-specific predicates that accept a tuple of constraints:

z3.integer((
    1 <= X <= 10,
    1 <= Y <= 10,
    X + Y == 10,
))

The () syntax is consistent with Clausal's goal tuples. Inside the block, standard Python operators (+, -, *, <, <=, ==, !=, >, >=) are interpreted under the declared theory. Unbound variables are automatically registered with the appropriate Z3 sort.

Chained comparisons work naturally: 1 <= X <= 10 becomes And(1 <= X, X <= 10).

Integer Constraints¶

z3.integer((...)) declares integer-sorted variables and posts constraints:

# skip
Schedule(T1, T2, T3) <- (
    z3.integer((
        0 <= T1 <= 100,
        0 <= T2 <= 100,
        0 <= T3 <= 100,
        T1 + 5 <= T2,
        T2 + 3 <= T3,
    )),
    z3.all_different([T1, T2, T3]),
    z3.label([T1, T2, T3]),
)

Labeling¶

z3.label(Vars) enumerates satisfying assignments. It is sort-polymorphic — it dispatches based on each variable's registered Z3 sort:

Sort	Behavior
IntSort	Blocking-clause enumeration (all solutions)
BoolSort	0/1 enumeration (all solutions)
BitVecSort	Blocking-clause enumeration (all solutions)
RealSort	Single model (continuous domain)
StringSort	Single model

# skip
Solve(X, Y) <- (
    z3.integer((1 <= X <= 3, 1 <= Y <= 3, X + Y == 4)),
    z3.label([X, Y]),
)
# yields (1, 3), (2, 2), (3, 1)

Global Constraints¶

Predicate	Description
`z3.all_different(Vars)`	All variables must have distinct values
`z3.table(Vars, Tuples)`	Extensional constraint — variables must match one of the given tuples
`z3.at_most(Vars, K)`	At most K boolean variables are true
`z3.at_least(Vars, K)`	At least K boolean variables are true
`z3.exactly(Vars, K)`	Exactly K boolean variables are true

Real Constraints¶

z3.real((...)) declares real-sorted variables. Z3 handles linear and non-linear real arithmetic:

# skip
Diet(Bread, Milk, Cost) <- (
    z3.real((
        0 <= Bread <= 100,
        0 <= Milk <= 100,
        2 * Bread + 3.5 * Milk >= 6,
    )),
    z3.minimize(2 * Bread + 3.5 * Milk, Cost),
)

Labeling real variables yields at most one satisfying assignment (continuous domains are not enumerable).

Boolean Constraints¶

z3.boolean((...)) declares boolean-sorted variables. Python's bitwise operators express boolean formulas:

# skip
Circuit(A, B, C) <- (
    z3.boolean((
        A | B,          # at least one is true
        ~(A & B & C),   # not all three
    )),
    z3.label([A, B, C]),
)

Bitvector Constraints¶

z3.bitvector(Width, (...)) declares fixed-width machine integers. Arithmetic wraps around and bitwise operations work naturally:

# skip
Mask(X, Result) <- (
    z3.bitvector(8, (
        X == 0xAB,
        X & 0xF0 == Result,
    )),
    z3.label([Result]),
)
# Result = 0xA0

Unsigned by Default¶

Comparisons inside z3.bitvector are unsigned:

X < Y means unsigned less-than (ULT)
X <= Y means unsigned less-or-equal (ULE)
X > Y means unsigned greater-than (UGT)
X >= Y means unsigned greater-or-equal (UGE)

Equality and disequality (==, !=) are sort-agnostic.

Structural Operations¶

Operations without Python operator equivalents are separate predicates:

Predicate	Description
`z3.extract(Hi, Lo, X, Result)`	Extract bits `[Hi:Lo]` from X
`z3.concat(X, Y, Result)`	Concatenate bitvectors (Result width = width(X) + width(Y))
`z3.zero_extend(X, N, Result)`	Zero-extend by N bits
`z3.sign_extend(X, N, Result)`	Sign-extend by N bits

Optimization¶

Maximize / Minimize¶

z3.maximize(Expr, Result) and z3.minimize(Expr, Result) find optimal values:

# skip
Optimal(X, Y, Cost) <- (
    z3.integer((
        0 <= X <= 10,
        0 <= Y <= 10,
        X + Y <= 10,
    )),
    z3.maximize(X + Y, Cost),
)
# Cost = 10

Soft Constraints¶

z3.soft(Constraint, Weight) adds a soft constraint. Soft constraints are satisfied if possible; when they conflict, Z3 maximizes total satisfied weight:

# skip
Preferences(X) <- (
    z3.integer((0 <= X <= 10)),
    z3.soft(X <= 3, 2),     # prefer X <= 3 (weight 2)
    z3.soft(X >= 7, 5),     # prefer X >= 7 (weight 5)
    z3.maximize_satisfaction(Satisfied),
)
# Satisfied = 5  (higher weight wins: X >= 7)

Optimize + Label¶

z3.optimize_label(Vars, Objective, Result, Mode) finds the optimal solution and binds variables in one step:

# skip
Schedule(T1, T2, T3, Cost) <- (
    z3.integer((
        0 <= T1 <= 100, 0 <= T2 <= 100, 0 <= T3 <= 100,
        T1 + 5 <= T2,
        T2 + 3 <= T3,
    )),
    z3.optimize_label([T1, T2, T3], T3, Cost, "minimize"),
)
# T1=0, T2=5, T3=8, Cost=8

Diagnostics¶

Satisfiability¶

Predicate	Description
`z3.check()`	Succeed if current constraints are satisfiable
`z3.satisfiability(Result)`	Unify Result with `"sat"`, `"unsat"`, or `"unknown"`
`z3.entailed(Constraint)`	Succeed if constraint is implied by the store
`z3.disentailed(Constraint)`	Succeed if constraint is impossible given the store

Unsat Cores¶

Named constraints enable debugging unsatisfiable constraint sets:

# skip
Debug(Core) <- (
    z3.integer((1 <= X <= 10)),
    z3.named(X > 8, "x_high"),
    z3.named(X < 3, "x_low"),
    z3.unsatisfiable_core(Core),
)
# Core = ["x_high", "x_low"]

Predicate	Description
`z3.named(Constraint, Name)`	Add a named constraint trackable via unsat core
`z3.unsatisfiable_core(Core)`	Get unsat core as a list of names (fails if sat)
`z3.minimal_unsatisfiable_core(Core)`	Get minimal unsat core (more expensive)

Inspection¶

Predicate	Description
`z3.model(Vars, Values)`	Get model as `[Name, Value]` pairs without binding variables
`z3.simplify(Expr, Result)`	Simplify a Z3 expression
`z3.assertions(List)`	Dump all Z3 assertions as strings
`z3.statistics(Stats)`	Get solver statistics as `[Key, Value]` pairs

Solver Configuration¶

Predicate	Description
`z3.set_option(Key, Value)`	Set solver option (e.g. `z3.set_option("timeout", 5000)`)
`z3.set_logic(Logic)`	Switch to logic-specific solver (e.g. `"QF_LIA"`, `"QF_BV"`)

Arrays, Sets, Strings¶

Arrays¶

Z3 arrays map indices to values (functional arrays with Select/Store):

Predicate	Description
`z3.array(Var, DomainSort, RangeSort)`	Declare an array variable
`z3.select(Array, Index, Value)`	Post `Select(Array, Index) == Value`
`z3.store(Array, Index, Value, Result)`	Post `Result == Store(Array, Index, Value)`
`z3.constant_array(Value, DomainSort, Result)`	Constant array mapping all indices to Value

Sets¶

Predicate	Description
`z3.set(Var, ElemSort)`	Declare a set variable
`z3.set_member(Elem, S)`	Post `Elem` in `S`
`z3.set_not_member(Elem, S)`	Post `Elem` not in `S`
`z3.set_subset(S1, S2)`	Post `S1` subset of `S2`
`z3.set_union(S1, S2, Result)`	Post `Result = S1 union S2`
`z3.set_intersect(S1, S2, Result)`	Post `Result = S1 intersect S2`
`z3.set_add(S, Elem, Result)`	Post `Result = S union {Elem}`

Strings¶

Predicate	Description
`z3.string(Var)`	Declare a string variable
`z3.string_length(S, N)`	Post `Length(S) == N`
`z3.string_contains(S, Sub)`	Post `Contains(S, Sub)`
`z3.string_concat(S1, S2, Result)`	Post `Result == Concat(S1, S2)`
`z3.string_regex(S, Pattern)`	Post `S` matches Z3 regex pattern

Uninterpreted Functions and Quantifiers¶

Uninterpreted Functions¶

Predicate	Description
`z3.function(Var, DomainSorts, RangeSort)`	Declare an uninterpreted function
`z3.apply(Func, Args, Result)`	Post `Result == Func(Args...)`

Z3 guarantees functional consistency: f(x) == f(y) whenever x == y.

Quantifiers¶

Predicate	Description
`z3.forall(VarSorts, BodyFn)`	Universal quantification
`z3.exists(VarSorts, BodyFn)`	Existential quantification

Algebraic Datatypes¶

Predicate	Description
`z3.declare_datatype(Name, Constructors)`	Declare a Z3 algebraic datatype

Comparison with Native CLP Solvers¶

Feature	CLP(Z)	CLP(R)	CLP(Q)	CLP(B)	Z3
Domain	integers	reals (interval)	rationals (exact)	booleans	all of these + BV, arrays, strings, ...
Solver	propagation + labeling	interval propagation	Gaussian + simplex	BDD	DPLL(T) + theory solvers
Non-linear	limited	interval splitting	rejects	n/a	full (non-linear real arithmetic)
Optimization	none	none	LP simplex	none	full (Optimize class)
Soft constraints	no	no	no	no	yes
Unsat cores	no	no	no	no	yes
External dep	none	none	none	none	`z3-solver`
Speed (small)	fastest	fast	fast	fast	overhead from Z3 FFI
Speed (large/complex)	limited	limited	good for LP	good for SAT	best for complex mixed theories

When to use Z3: complex problems mixing multiple theories, optimization with soft constraints, problems requiring unsat core explanations, bitvector reasoning (hardware verification, cryptography), string constraints, or any problem where native CLP solvers are insufficient.

When to prefer native CLP: simple integer/boolean/rational problems where startup overhead matters, or when you want zero external dependencies.

Complete Predicate Reference¶

Theory Declaration¶

Predicate	Arity	Description
`z3.integer`	1	`z3.integer((constraints))` — post integer constraints
`z3.real`	1	`z3.real((constraints))` — post real constraints
`z3.boolean`	1	`z3.boolean((constraints))` — post boolean constraints
`z3.bitvector`	2	`z3.bitvector(Width, (constraints))` — post bitvector constraints

Solving¶

Predicate	Arity	Description
`z3.label`	1	Sort-polymorphic labeling
`z3.check`	0	Satisfiability check
`z3.all_different`	1	Distinct constraint
`z3.table`	2	Extensional (table) constraint

Optimization¶

Predicate	Arity	Description
`z3.maximize`	2	Maximize expression
`z3.minimize`	2	Minimize expression
`z3.soft`	2, 3	Add soft constraint (with optional group)
`z3.maximize_satisfaction`	1	MaxSAT — maximize satisfied soft weight
`z3.optimize_label`	4	Optimize + label in one step

Diagnostics¶

Predicate	Arity	Description
`z3.satisfiability`	1	Result is `"sat"`, `"unsat"`, or `"unknown"`
`z3.entailed`	1	Succeed if constraint is implied
`z3.disentailed`	1	Succeed if constraint is impossible
`z3.named`	2	Add named constraint for unsat core
`z3.unsatisfiable_core`	1	Get unsat core as list of names
`z3.minimal_unsatisfiable_core`	1	Get minimal unsat core
`z3.model`	2	Get model without binding variables
`z3.simplify`	2	Simplify expression
`z3.assertions`	1	Dump constraint store
`z3.statistics`	1	Get solver statistics
`z3.set_option`	2	Set solver option
`z3.set_logic`	1	Switch to logic-specific solver