SIGN IN SIGN UP

[Compiler][Z3] Bump 3rdparty/tvm to materialize Z3 solvers lazily (#3105)

* [Compiler][Z3] Bump 3rdparty/tvm to materialize Z3 solvers lazily

Z3Prover::Impl created a z3::solver eagerly in the Analyzer constructor
and translated every Bind/EnterConstraint into z3 constraints up front.
Analyzers are scratch objects created in huge numbers during lowering (a
reducer-heavy kernel compile creates ~67k of them, ~100k binds), while
only ~0.3% ever reach the Z3 fallback of CanProve, so the eager setup
dominated layout-inference-heavy compiles.

With the bump, binds and constraints are journaled and the solver is
created and replayed on first use. End-to-end compile of the worst
regressing reducer kernels drops 40-60%, and tilelang.lower roughly
halves across the board. Language suite 1168 passed / 137 skipped,
reducer_v2 75 passed, arith 89 passed; generated CUDA byte-identical
under disabled ASLR.

tvm changeset: https://github.com/tile-ai/tvm/pull/68

* [Cleanup] Drop Z3ContextScope wrappers

With the bumped tvm, every materialized Z3 solver owns a private context
(tile-ai/tvm#69), which subsumes the per-compilation isolation these
scopes provided; the scope functions are now documented no-ops. Remove
the wrappers around lowering and grouped compilation, and rewrite the
scope-lifetime arith test to assert what it actually guarded: a cloned
Analyzer's Z3 handles stay valid after the source is destroyed.

Validation (cold caches): layout suite 298 passed (including the
z3-context isolation tests, which cover the grouped-compile path),
language suite 1172 passed / 137 skipped, arith 89 passed, reducer_v2
75 passed.

* Point 3rdparty/tvm at the merged lazy-Z3 changes

tile-ai/tvm#68 and tile-ai/tvm#69 are both merged; replace the PR-branch
pin with the tilelang_main commit.
L
Lei Wang committed
a1f8ebd4ed9caa4a579fec1eafe873be452a0860
Parent: 8ef052f
Committed by GitHub <noreply@github.com> on 8/28/2026, 4:51:12 PM