Z3 SMT Solver¶
Z3 is a high-performance Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Clausal Prolog's Z3 integration exposes Z3's multi-theory solver as constraint predicates under the z3.* module namespace.
Unlike Clausal Prolog'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. Every example on this page was run
against z3-solver 4.15.
Constraint Blocks¶
Constraints are posted via theory-specific predicates that accept a tuple of constraints:
The () syntax is consistent with the seam'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:
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]),
)
# e.g. (0, 5, 8), (1, 6, 9), ...; blocking-clause enumeration, in the order Z3 finds them
Querying from Python¶
In a .seam file, query with a goal-position -- (from a function; a query at module
top level runs before the predicates are registered):
pairs(X, Y) <- (
z3.integer((1 <= X <= 3, 1 <= Y <= 3, X + Y == 4)),
z3.label([X, Y]),
)
def main():
for X, Y in --pairs(X, Y):
print(X, Y) # 1 3, 2 2 and 3 1, in the order Z3 finds them
Only bound variables can be exported. A variable that is still a Z3 unknown — one the
goal never labels, or one z3.maximize/2 optimised without binding — raises
ResidualConstraints (from clausal.logic.seam). Export the variables the goal binds
(for C in --optimal(_X, _Y, C)), label the rest inside the goal, or read the model with
z3.model/2.
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 |
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), in the order Z3 finds them
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:
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),
)
# COST = 6; BREAD and MILK stay Z3 unknowns (minimize binds only 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:
circuit(A, B, C) <- (
z3.boolean((
A | B, # at least one is true
~(A & B & C), # not all three
)),
z3.label([A, B, C]),
)
# yields every 0/1 triple satisfying both formulas, in the order Z3 finds them
Bitvector Constraints¶
z3.bitvector(Width, (...)) declares fixed-width machine integers. Arithmetic wraps around and bitwise operations work naturally:
mask(X, RESULT) <- (
z3.bitvector(8, (
X == 0xAB,
X & 0xF0 == RESULT,
)),
z3.label([RESULT]),
)
# RESULT = 160 (0xA0); X is not labelled, so it stays a Z3 unknown
Unsigned by Default¶
Comparisons inside z3.bitvector are unsigned:
X < Ymeans unsigned less-than (ULT)X <= Ymeans unsigned less-or-equal (ULE)X > Ymeans unsigned greater-than (UGT)X >= Ymeans 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:
optimal(X, Y, COST) <- (
z3.integer((
0 <= X <= 10,
0 <= Y <= 10,
X + Y <= 10,
)),
z3.maximize(X + Y, COST),
)
# COST = 10 (X and Y are not bound; z3.optimize_label/4 binds them)
Soft Constraints¶
z3.soft(Constraint, Weight) adds a soft constraint. Soft constraints are satisfied if possible; when they conflict, Z3 maximizes total satisfied weight:
preferences(X, SATISFIED) <- (
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:
schedule_min(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 the atom 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:
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 (Name is an atom, Value a number or boolean) |
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') |
Key and Logic are names, so they are atoms: write them single-quoted
(or bare and declared). A double-quoted "timeout" is a string under the
default -double_quotes(chars), and a string there is a
type_error(atom, …), the same answer z3.named/2 gives.
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 |
The datatype name, every constructor name and every field name are names (atoms); a field whose sort is written as the datatype's own name is the self-reference form:
declare_int_list() <- z3.declare_datatype('IntList', [
('nil', []),
('cons', [('head', 'IntList')]),
])
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 the atom 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 |