How Deppy Uses Z3

Z3 as a leaf solver: encoding Python into SMT, controlling the solver, and debugging failures.

If you have used F*, you know that Z3 is the primary decision procedure — essentially every proof obligation is shipped to Z3 as a first-order logic formula. Deppy takes a different approach: Z3 is a leaf solver embedded inside the homotopy proof search. The top-level proof structure is always a homotopy proof term (paths, transport, Čech gluing), but whenever the search reaches a sub-goal that is a decidable arithmetic, boolean, or quantifier-free formula, it hands that goal to Z3.

This chapter explains exactly how Deppy encodes Python types and expressions into Z3's input language (SMT-LIB 2), how to control the solver, and how to debug when things go wrong.

Z3's Role in the Pipeline

Recall the verification pipeline from the Overview:

                     ┌──────────────────────────┐
                     │   HomotopyStrategy       │
                     │                          │
  ProofGoal ────────▶│  try_refl()              │
                     │  try_congruence()        │
                     │  try_transport()         │
                     │  try_cech()              │
                     │  try_funext()            │
                     │  try_z3_leaf() ──────────│──▶  Z3 Solver
                     │                          │       │
                     │          ◀───────────────│───────┘
                     │       Z3Leaf(cert)       │
                     └──────────────────────────┘

Z3 is invoked in two contexts:

1. As a leaf solver — When HomotopyStrategy.try_z3_leaf() is called, the current sub-goal is encoded as an SMT query and sent to Z3. If Z3 returns unsat (the negation of the goal is unsatisfiable), the goal is proved and a Z3Leaf proof term is emitted.
2. As a direct strategy — For goals classified as Z3Only by the dispatcher (purely arithmetic/boolean refinements), Z3 is called directly without homotopy wrapping.

Python-to-Z3 Encoding

The Z3Encoder class translates Python types, expressions, and constraints into Z3 sorts, terms, and assertions. This is the most delicate part of the Z3 integration: if the encoding is unsound, the entire system's guarantees collapse. For this reason, the encoder is extensively tested and its soundness is documented with respect to Python's semantics.

Scalar Types

# Python int → Z3 Int
from z3 import Int, IntSort

x = Int('x')    # Z3 integer variable named 'x'

# Corresponding SMT-LIB:
; (declare-const x Int)

# Python bool → Z3 Bool
from z3 import Bool, And, Or, Not

flag = Bool('flag')
constraint = And(flag, Not(Bool('other')))

; (declare-const flag Bool)
; (declare-const other Bool)
; (assert (and flag (not other)))

Collection Types

# list[int] → Z3 Seq(IntSort())
from z3 import SeqSort, IntSort, Const, Length, Unit, Concat
def Nth(seq, idx): return seq[idx]  # z3 sequence indexing

IntSeq = SeqSort(IntSort())
xs = Const('xs', IntSeq)

# len(xs) → Length(xs)
# xs[i]   → Nth(xs, i)
# xs + ys → Concat(xs, ys)

; SMT-LIB encoding:
; (declare-const xs (Seq Int))
; (assert (> (seq.len xs) 0))
; (assert (>= (seq.nth xs 0) 0))

# dict[str, int] → Z3 Array(StringSort(), IntSort())
from z3 import Array, StringSort, IntSort, Select, Store

d = Array('d', StringSort(), IntSort())

# d["key"]       → Select(d, StringVal("key"))
# d["key"] = 42  → Store(d, StringVal("key"), IntVal(42))

; (declare-const d (Array String Int))
; (assert (= (select d "key") 42))

Python Classes → Z3 Datatypes

Python classes with type-annotated fields are encoded as Z3 algebraic datatypes. Each field becomes a selector, and the class constructor becomes a Z3 constructor:

# Python class
class Point:
    x: int
    y: int

# Z3 encoding
Point = Datatype('Point')
Point.declare('mk_point', ('x', IntSort()), ('y', IntSort()))
Point = Point.create()

mk_point = Point.mk_point
get_x = Point.x
get_y = Point.y

; SMT-LIB:
; (declare-datatypes ((Point 0))
;   (((mk_point (x Int) (y Int)))))
;
; (declare-const p Point)
; (assert (= (x p) 3))
; (assert (= (y p) 4))

Python Functions → Z3 Uninterpreted Functions

When a function appears in a refinement but its body is not being analyzed (e.g., it's a library function), Deppy encodes it as a Z3 uninterpreted function — Z3 knows the function's type signature but nothing about its implementation. Any known properties (from @guarantee decorators or sidecar proofs) are added as axioms:

# Python function (body not analyzed by Z3)
@guarantee("result == len(xs) + len(ys)")
def total_length(xs: list[int], ys: list[int]) -> int:
    ...

# Z3 encoding
total_length = Function(
    'total_length',
    SeqSort(IntSort()),   # xs
    SeqSort(IntSort()),   # ys
    IntSort()             # return type
)

# Add the guarantee as an axiom
xs = Const('xs', SeqSort(IntSort()))
ys = Const('ys', SeqSort(IntSort()))
solver.add(ForAll(
    [xs, ys],
    total_length(xs, ys) == Length(xs) + Length(ys)
))

; SMT-LIB:
; (declare-fun total_length ((Seq Int) (Seq Int)) Int)
; (assert (forall ((xs (Seq Int)) (ys (Seq Int)))
;   (= (total_length xs ys) (+ (seq.len xs) (seq.len ys)))))

Quantifier Encoding

Quantifiers are the most challenging part of SMT solving. Z3 uses an E-matching strategy for quantifier instantiation, which means it needs trigger patterns to know when to instantiate a universal quantifier. Deppy carefully generates these triggers.

Universal Quantification

# Python: "for all i in range(len(xs)), xs[i] >= 0"
# This comes from: @guarantee("all elements are non-negative")

# Z3 encoding with explicit trigger pattern
i = Int('i')
xs = Const('xs', SeqSort(IntSort()))

forall_constraint = ForAll(
    [i],
    Implies(
        And(0 <= i, i < Length(xs)),
        Nth(xs, i) >= 0
    ),
    patterns=[MultiPattern(Nth(xs, i))]  # trigger on xs[i]
)

# SMT-LIB equivalent:
# (assert
#   (forall ((i Int))
#     (! (=> (and (<= 0 i) (< i (seq.len xs)))
#            (>= (seq.nth xs i) 0))
#        :pattern ((seq.nth xs i)))))

Existential Quantification

# Python: "there exists an i such that xs[i] == target"
# from: @guarantee("target is found in the list")

i = Int('i')
target = Int('target')
xs = Const('xs', SeqSort(IntSort()))

exists_constraint = Exists(
    [i],
    And(
        0 <= i,
        i < Length(xs),
        Nth(xs, i) == target
    )
)

# SMT-LIB equivalent:
# (assert
#   (exists ((i Int))
#     (and (<= 0 i)
#          (< i (seq.len xs))
#          (= (seq.nth xs i) target))))

Pattern-Based Triggering in Depth

Triggers (also called patterns) control quantifier instantiation in Z3's E-matching engine. A trigger is a set of ground terms that, when they appear in the E-graph (the solver's equality saturation structure), cause the quantifier to be instantiated with matching substitutions.

# Example: a sortedness property with two triggers
# "for all i, j: i < j implies xs[i] <= xs[j]"

i, j = Ints('i j')
xs = Const('xs', SeqSort(IntSort()))

sorted_prop = ForAll(
    [i, j],
    Implies(
        And(0 <= i, i < j, j < Length(xs)),
        Nth(xs, i) <= Nth(xs, j)
    ),
    patterns=[MultiPattern(Nth(xs, i), Nth(xs, j))]
)

# SMT-LIB equivalent:
# (assert
#   (forall ((i Int) (j Int))
#     (! (=> (and (<= 0 i) (< i j) (< j (seq.len xs)))
#            (<= (seq.nth xs i) (seq.nth xs j)))
#        :pattern ((seq.nth xs i) (seq.nth xs j)))))

The MultiPattern here says: "instantiate this quantifier whenever both xs[i] and xs[j] appear in the E-graph for some concrete i and j." This is more restrictive than a single-pattern trigger and avoids the combinatorial explosion that would result from triggering on xs[i] alone.

When Z3 Succeeds Immediately

Z3 can decide goals in certain decidable fragments of first-order logic without any help from the homotopy engine. Deppy recognizes these fragments and routes them directly to Z3:

# Example: QF_LIA — Z3 solves this instantly

@guarantee("result == a + b")
def add(a: int, b: int) -> int:
    return a + b

# Generated Z3 query:
; (declare-const a Int)
; (declare-const b Int)
; (declare-const result Int)
; (assert (= result (+ a b)))   ; function body
; (assert (not (= result (+ a b))))  ; negated postcondition
; (check-sat)  → unsat  ✓  (postcondition holds)

When Z3 Needs Help

Many real-world proof obligations fall outside the decidable fragments. When Z3 returns unknown or times out, Deppy's homotopy engine takes over. Common scenarios:

Non-Linear Arithmetic

# Z3 struggles with non-linear integer arithmetic
@guarantee("result == n * (n + 1) // 2")
def triangle(n: int) -> int:
    assume("n >= 0")
    total = 0
    for i in range(n + 1):
        total += i
    return total

# The loop invariant involves n*i, which is non-linear.
# Z3 alone may time out. Deppy's homotopy engine:
#   1. Unrolls the loop conceptually as a path (n steps)
#   2. Proves each step via Z3 (linear: total' = total + i)
#   3. Composes the path steps via PathComp
#   4. Final composition proves the full invariant

Inductive Properties

# Induction is not built into Z3's core
@guarantee("result == xs[::-1][::-1]")
def reverse_involution(xs: list[int]) -> list[int]:
    return xs

# Deppy proves this by structural induction on the list:
#   Base case (empty list):  Z3 leaf
#   Inductive step:         Homotopy + Z3 leaf
#   Composition:            PathComp over the induction structure

Higher-Order Functions

# Z3 cannot reason about function equality
@guarantee("map(f, map(g, xs)) == map(compose(f, g), xs)")
def map_fusion(
    f: Callable[[int], int],
    g: Callable[[int], int],
    xs: list[int]
) -> bool:
    return True

# Deppy uses FunExt (function extensionality):
#   1. Reduce to pointwise: for each element x in xs,
#      f(g(x)) == compose(f,g)(x)
#   2. That's true by definition of compose → Refl
#   3. FunExt lifts to the list level
#   4. Induction over the list length glues it all

Controlling Z3

Timeout Settings

# Programmatic control via deppy.config:
from deppy.config import DeppyConfig

config = DeppyConfig(
    z3_timeout=10000,         # per-query timeout (ms)
    z3_rlimit=10_000_000,       # Z3 resource budget (deterministic)
    trust_level="Z3_PROVEN",
    parallel=True,
    lean_export=True,
)

Resource Limits

# Z3 supports resource limits (rlimit) as an alternative to timeouts.
# Resource limits are deterministic — the same query always uses the
# same number of resources regardless of machine speed.
#
# Set them via deppy.config.DeppyConfig.z3_rlimit (default 10M),
# or directly on a z3 Solver below.

# Programmatic control
from z3 import Solver, set_param

solver = Solver()
solver.set("timeout", 5000)
solver.set("rlimit", 2000000)

# SMT-LIB equivalent:
# (set-option :timeout 5000)
# (set-option :rlimit 2000000)

Custom Tactics

Z3's tactic framework lets you compose proof strategies. Deppy exposes this for advanced users:

# Deppy default tactic pipeline for arithmetic goals
from z3 import Then, Tactic, OrElse

default_tactic = Then(
    Tactic('simplify'),         # Algebraic simplification
    Tactic('propagate-values'), # Constant propagation
    Tactic('solve-eqs'),        # Gaussian elimination
    OrElse(
        Tactic('qflia'),         # QF_LIA decision procedure
        Tactic('smt')            # General SMT fallback
    )
)

# For non-linear arithmetic, Deppy switches to:
nla_tactic = Then(
    Tactic('simplify'),
    Tactic('nla2bv'),           # Try bit-blasting
    Tactic('sat')
)

; SMT-LIB:
; (check-sat-using (then simplify propagate-values solve-eqs
;                   (or-else qflia smt)))

Incremental Solving

When verifying a function with multiple proof obligations, Deppy uses Z3's incremental solving feature. Shared context (parameter types, preconditions, class invariants) is asserted once, and individual goals are checked using push/pop scopes:

# Incremental solving for a function with 3 proof obligations

solver = Solver()

# Shared context (asserted once)
x = Int('x')
solver.add(x > 0)     # precondition: assume("x > 0")
solver.add(x < 100)   # precondition: assume("x < 100")

# Goal 1: x + 1 > 0
solver.push()
solver.add(Not(x + 1 > 0))  # negate the goal
result1 = solver.check()       # → unsat ✓
solver.pop()

# Goal 2: x * 2 < 200
solver.push()
solver.add(Not(x * 2 < 200))
result2 = solver.check()       # → unsat ✓
solver.pop()

# Goal 3: x - 1 >= 0
solver.push()
solver.add(Not(x - 1 >= 0))
result3 = solver.check()       # → unsat ✓
solver.pop()

; SMT-LIB:
; (declare-const x Int)
; (assert (> x 0))
; (assert (< x 100))
;
; (push 1)
; (assert (not (> (+ x 1) 0)))
; (check-sat)  ; → unsat
; (pop 1)
;
; (push 1)
; (assert (not (< (* x 2) 200)))
; (check-sat)  ; → unsat
; (pop 1)
;
; (push 1)
; (assert (not (>= (- x 1) 0)))
; (check-sat)  ; → unsat
; (pop 1)

The T.z3_auto() tactic

At the tactic-DSL level (deppy.proofs.language.T), the recommended Z3 entry point is T.z3_auto(). Unlike T.z3(formula), it doesn't require the user to restate the goal as a string — it reads the current goal off the ProofBuilder:

• Equality goal ``lhs = rhs`` → formula ``"lhs == rhs"``
• Refinement goal ``{x | P(x)}`` → formula ``P(x)``
• Other goal shapes → an explicit ``formula`` argument is required

The inferred formula is parsed by Python's ``compile()`` *eagerly*, so a syntactically broken formula raises immediately when T.z3_auto() is called — i.e., at the moment the proof script first builds the tactic, before any solver is invoked — rather than emerging from inside Z3 later. After parsing, the tactic delegates to the same kernel _verify_z3 path described above, with the same error codes (E005 / E005b / E005c / E005i).

from deppy.proofs.language import T, eq, prove
from deppy.core.kernel import ProofKernel

kernel = ProofKernel()
goal = eq("x * x", "x * x", x="int")
result = prove("refl_via_z3", kernel=kernel, goal=goal,
               tactic=T.z3_auto())
# result.trust_level → Z3_VERIFIED on success

Debugging Z3 Failures

When Z3 returns unknown or sat (meaning the negated goal is satisfiable, i.e., there's a counterexample), you need to understand why. Deppy provides several tools for this.

Reading Unsat Cores

An unsat core is a minimal subset of assertions that is sufficient to prove unsatisfiability. When Z3 succeeds, you can ask for the core to understand which assumptions were actually used:

# Enable unsat core tracking
solver = Solver()
solver.set("unsat_core", True)

# Name each assertion
p1 = Bool('p1')  # "x > 0"
p2 = Bool('p2')  # "x < 100"
p3 = Bool('p3')  # "y == x + 1"

solver.assert_and_track(x > 0, p1)
solver.assert_and_track(x < 100, p2)
solver.assert_and_track(y == x + 1, p3)
solver.add(Not(y > 0))  # negated goal

result = solver.check()  # → unsat
core = solver.unsat_core()
print(core)  # → [p1, p3]  (p2 was not needed)

; SMT-LIB:
; (set-option :produce-unsat-cores true)
; (assert (! (> x 0) :named p1))
; (assert (! (< x 100) :named p2))
; (assert (! (= y (+ x 1)) :named p3))
; (assert (not (> y 0)))
; (check-sat)        ; → unsat
; (get-unsat-core)   ; → (p1 p3)

Generating Counterexamples

When Z3 returns sat, it means the postcondition can be violated. Z3 provides a model — concrete values that demonstrate the violation:

# A buggy function
@guarantee("result > 0")
def buggy_abs(x: int) -> int:
    return x  # Bug: doesn't handle negative x

# Z3 query
solver = Solver()
x = Int('x')
result = Int('result')
solver.add(result == x)         # function body
solver.add(Not(result > 0))     # negated postcondition

check = solver.check()          # → sat (counterexample exists!)
model = solver.model()
print(model)                    # → [x = -1, result = -1]

# Deppy reports:
# ❌ Verification failed for buggy_abs
#    Postcondition: result > 0
#    Counterexample: x = -1 → result = -1
#    The returned value -1 is not > 0

The Z3 Proof Trace

For deep debugging, Z3 can produce a full proof trace that shows how it derived unsat. Deppy can export this trace for inspection:

# Enable proof production
set_param("proof", True)

solver = Solver()
solver.add(x > 0)
solver.add(x < 0)
result = solver.check()  # → unsat
print(f"result: {result}")

try:
    proof = solver.proof()
    print(proof)
    # mp(asserted(x > 0),
    #    asserted(x < 0),
    #    trans(leq-axiom(...), ...),
    #    false)
except Exception:
    print("(proof object not available — depends on Z3 build)")

# Export to SMT-LIB for inspection
print(solver.to_smt2()[:200])

Example: Step-by-Step Refinement Check

Let's trace the complete Z3 encoding of a refinement type check:

@guarantee("result is sorted and has same length as input")
def insertion_sort(xs: list[int]) -> list[int]:
    result = list(xs)
    for i in range(1, len(result)):
        key = result[i]
        j = i - 1
        while j >= 0 and result[j] > key:
            result[j + 1] = result[j]
            j -= 1
        result[j + 1] = key
    return result

; (declare-const xs (Seq Int))
; (declare-const result (Seq Int))

; (assert (= (seq.len result) (seq.len xs)))
; ; from the loop structure analysis: the loop only swaps,
; ; never adds or removes elements

; Loop invariant at iteration k:
; (forall ((p Int) (q Int))
;   (! (=> (and (<= 0 p) (< p q) (<= q k))
;          (<= (seq.nth result p) (seq.nth result q)))
;      :pattern ((seq.nth result p) (seq.nth result q))))

Example: Quantifier Instantiation for Array Bounds

Array bounds checking is one of the most common verification tasks. Here's how Deppy encodes and verifies a safe array access:

@guarantee("no index-out-of-bounds")
def safe_sum(xs: list[int], indices: list[int]) -> int:
    assume("all elements of indices are valid: 0 <= i < len(xs)")
    total = 0
    for idx in indices:
        total += xs[idx]   # Need to prove: 0 <= idx < len(xs)
    return total

; Z3 encoding of the bounds check at xs[idx]

; Declarations
(declare-const xs (Seq Int))
(declare-const indices (Seq Int))
(declare-const k Int)               ; loop iteration variable

; Precondition: all indices are valid
(assert
  (forall ((j Int))
    (! (=> (and (<= 0 j) (< j (seq.len indices)))
           (and (<= 0 (seq.nth indices j))
                (< (seq.nth indices j) (seq.len xs))))
       :pattern ((seq.nth indices j)))))

; Current iteration: idx = indices[k]
(assert (and (<= 0 k) (< k (seq.len indices))))

; Goal (negated): is the access xs[indices[k]] in-bounds?
(assert
  (not (and (<= 0 (seq.nth indices k))
            (< (seq.nth indices k) (seq.len xs)))))

; (check-sat)
; → unsat
;
; Z3 instantiates the forall with j ↦ k (triggered by
; the pattern (seq.nth indices k)), yielding:
;   0 <= k < len(indices) →
;     0 <= indices[k] < len(xs)
; Combined with the assertion 0 <= k < len(indices),
; this contradicts the negated goal. QED.

Example: Z3 + Homotopy Collaboration

The most interesting verification scenarios involve both Z3 and the homotopy engine working together. Here's a function where Z3 handles the arithmetic leaves and homotopy provides the structural glue:

@guarantee("result preserves the sum: sum(result) == sum(xs)")
@guarantee("result is sorted")
def verified_sort(xs: list[int]) -> list[int]:
    if len(xs) <= 1:
        return xs
    mid = len(xs) // 2
    left = verified_sort(xs[:mid])
    right = verified_sort(xs[mid:])
    return merge(left, right)

CechGlue(
  patches=[
    Patch(domain="len ≤ 1", proof=Refl()),
    Patch(domain="len > 1", proof=Trans(
      Trans(Z3Leaf(cert_1), Z3Leaf(cert_2)),
      Z3Leaf(cert_3)
    ))
  ],
  gluing=Z3Leaf(cert_overlap)
)

This example illustrates the division of labor: the homotopy engine provides the proof architecture (Čech decomposition, transitivity chains), while Z3 handles the arithmetic facts at the leaves.

Z3 Encoding of Homotopy Constructs

Although Z3 doesn't natively understand homotopy type theory, Deppy sometimes needs to encode homotopy-adjacent concepts into Z3 for leaf-level reasoning. Three specialized encoders handle this:

PathEncoder: Paths as Z3 Functions

A path Path A a b can be thought of as a function f : [0,1] → A with f(0) = a and f(1) = b. When Z3 needs to reason about path properties, Deppy encodes them as uninterpreted functions over the real interval:

# PathEncoder: encode a path as a Z3 function

import z3
from z3 import Function, RealSort, IntSort, ForAll, Real, Implies, And

class PathEncoder:
    def encode_path(
        self,
        name: str,
        sort: z3.SortRef,
        start: z3.ExprRef,
        end: z3.ExprRef
    ) -> tuple:
        # Path as a function from [0,1] to the sort
        path_fn = Function(name, RealSort(), sort)
        t = Real('t')

        constraints = [
            path_fn(0) == start,  # left endpoint
            path_fn(1) == end,    # right endpoint
            # Continuity (approximated): nearby inputs → nearby outputs
            ForAll([t],
                Implies(
                    And(0 <= t, t <= 1),
                    And(sort.lo <= path_fn(t),
                         path_fn(t) <= sort.hi)
                )
            )
        ]
        return path_fn, constraints

; SMT-LIB:
; (declare-fun path_p (Real) Int)
; (assert (= (path_p 0.0) 3))    ; start
; (assert (= (path_p 1.0) 5))    ; end
; (assert (forall ((t Real))
;   (=> (and (<= 0.0 t) (<= t 1.0))
;       (and (<= 0 (path_p t)) (<= (path_p t) 1000)))))

TransportEncoder: Transport as Function Composition

Transport along a path p : Path Type A B carries a value x : A to a value transport(p, x) : B. When the types A and B have Z3 encodings, transport becomes a function composition:

import z3

class TransportEncoder:
    def encode_transport(
        self,
        type_path: PathEncoder,
        value: z3.ExprRef,
        coercion: z3.FuncDeclRef
    ) -> z3.ExprRef:
        """
        Encode transport(p, x) as coercion(x).

        The coercion function witnesses the equivalence
        between the source and target types.
        """
        return coercion(value)

# Example: transport along int ≃ nat (for non-negative ints)
# coercion: x ↦ x (identity, since nat ⊆ int in Z3)

; SMT-LIB:
; (declare-fun coerce_int_nat (Int) Int)
; (assert (forall ((x Int))
;   (=> (>= x 0) (= (coerce_int_nat x) x))))
; ; transport(path_int_nat, 42) = coerce_int_nat(42) = 42

CechEncoder: Patches as Array Partitions

A Čech cover decomposes a domain into overlapping patches. When the domain is an integer range (e.g., array indices), the patches become sub-ranges, and the covering condition becomes an array partition property:

import z3
from z3 import Int, Or, And, ForAll, Implies
from itertools import combinations

class CechEncoder:
    def encode_cover(
        self,
        domain_size: z3.ExprRef,
        patches: list[tuple[z3.ExprRef, z3.ExprRef]]
    ) -> list[z3.ExprRef]:
        """
        Encode covering condition: every index is in at least
        one patch.
        """
        constraints = []
        i = Int('i')

        # Covering: ∀ i ∈ [0, n), ∃ patch containing i
        patch_contains = Or(*[
            And(lo <= i, i < hi)
            for lo, hi in patches
        ])
        constraints.append(
            ForAll([i],
                Implies(
                    And(0 <= i, i < domain_size),
                    patch_contains
                )
            )
        )

        # Overlap agreement: on shared indices, patch proofs agree
        for (lo1, hi1), (lo2, hi2) in combinations(patches, 2):
            overlap = And(
                And(lo1 <= i, i < hi1),
                And(lo2 <= i, i < hi2)
            )
            # Agreement on overlaps is checked separately

        return constraints

; SMT-LIB for a 2-patch cover of [0, n):
; patch 1: [0, mid)    patch 2: [mid-1, n)    overlap: [mid-1, mid)
;
; (declare-const n Int)
; (declare-const mid Int)
; (assert (> n 0))
; (assert (= mid (div n 2)))
;
; ; Covering condition
; (assert (forall ((i Int))
;   (=> (and (<= 0 i) (< i n))
;       (or (and (<= 0 i) (< i mid))
;           (and (<= (- mid 1) i) (< i n))))))
;
; (check-sat)  ; → unsat (covering holds)

The Z3Encoder: Full Implementation Sketch

For reference, here is a condensed view of the complete Z3Encoder class that ties together all the encoding strategies:

class Z3Encoder:
    """Encode Python types, expressions, and constraints into Z3."""

    def __init__(self):
        self.sort_cache: dict[SynType, z3.SortRef] = {}
        self.func_cache: dict[str, z3.FuncDeclRef] = {}
        self.path_encoder = PathEncoder()
        self.transport_encoder = TransportEncoder()
        self.cech_encoder = CechEncoder()

    def encode_type(self, ty: SynType) -> z3.SortRef:
        if ty in self.sort_cache:
            return self.sort_cache[ty]

        match ty:
            case IntType():     sort = IntSort()
            case BoolType():    sort = BoolSort()
            case StrType():     sort = StringSort()
            case FloatType():   sort = RealSort()
            case ListType(elem):
                sort = SeqSort(self.encode_type(elem))
            case DictType(k, v):
                sort = ArraySort(
                    self.encode_type(k),
                    self.encode_type(v)
                )
            case ClassType(name, fields):
                sort = self._encode_datatype(name, fields)
            case FunctionType(params, ret):
                sort = self._encode_function_sort(params, ret)
            case _:
                raise EncodingError(f"Cannot encode {ty}")

        self.sort_cache[ty] = sort
        return sort

    def encode_expr(self, expr: Expr, env: dict) -> z3.ExprRef:
        match expr:
            case IntLit(n):      return IntVal(n)
            case BoolLit(b):     return BoolVal(b)
            case StrLit(s):      return StringVal(s)
            case Var(name):       return env[name]
            case BinOp(l, "+", r):
                return self.encode_expr(l, env) + self.encode_expr(r, env)
            case BinOp(l, "<", r):
                return self.encode_expr(l, env) < self.encode_expr(r, env)
            case Call(func, args):
                z3_func = self._get_or_create_func(func)
                z3_args = [self.encode_expr(a, env) for a in args]
                return z3_func(*z3_args)
            # ... more cases ...

    def encode_goal(self, goal: ProofGoal) -> z3.ExprRef:
        """Encode a proof goal as a Z3 assertion (negated for refutation)."""
        env = {}
        for hyp in goal.context:
            z3_var = Const(hyp.name, self.encode_type(hyp.type))
            env[hyp.name] = z3_var

        z3_goal = self.encode_expr(goal.goal_type.to_expr(), env)
        return Not(z3_goal)  # negate: unsat means goal holds

Summary

Z3 in Deppy is a precision instrument, not a blunt hammer. Rather than sending every proof obligation to an SMT solver and hoping it works, Deppy uses Z3 surgically — only for the decidable arithmetic, boolean, and quantifier-free fragments where Z3 excels. The homotopy engine handles the structural reasoning (equality, transport, decomposition), and Z3 handles the numeric facts at the leaves. This division of labor means:

• Z3 almost always succeeds — because it only sees goals in its sweet spot.
• Timeout failures are rare — because undecidable fragments are never sent to Z3.
• Proof terms are always produced — even when Z3 is used, the result is wrapped in a Z3Leaf that the kernel can verify.
• The system degrades gracefully — if Z3 fails on a leaf, the homotopy engine can try alternative decompositions or ask for a manual sidecar proof.