---
id: pr-tilelang-1367
repo: tile-ai/tilelang
pr: 1367
title: '[Feat] Integrate Z3 in TVM Arith Analyzer'
author: kurisu6912
date: '2025-12-17'
url: https://github.com/tile-ai/tilelang/pull/1367
source_category: upstream-code
architectures:
- sm90
tags:
- sm90
- triton kernel
techniques: []
hardware_features:
- hopper
kernel_types: []
languages:
- cuda-cpp
- triton
captured_at: '2026-05-16'
status: merged
merge_sha: 9c21586b54cde5dd7449f5471502983b5f66d9c7
inclusion_reason: Search-matched CUDA kernel optimization PR; materialize diff/source before synthesis.
changed_paths:
- 3rdparty/tvm
- CMakeLists.txt
- cmake/pypi-z3/FindZ3.cmake
- pyproject.toml
- requirements-dev.txt
- requirements-test.txt
- requirements.txt
- testing/python/arith/test_arith_hard.py
- testing/python/arith/test_arith_intset.py
- testing/python/arith/test_arith_iter_affine_map.py
- testing/python/arith/test_arith_simplify.py
- testing/python/tilelibrary/test_tilelang_tilelibrary_gemm_sp.py
- testing/python/transform/test_tilelang_transform_legalize_safe_memory_access.py
- tilelang/language/reduce.py
- tilelang/utils/sparse.py
artifact_dir: evidence/pull-bundles/tilelang/gh-1367
head_ref_oid: 0fc85499f0883bf606b10fe71e79d13604c3493f
---
# [Feat] Integrate Z3 in TVM Arith Analyzer

- Repository: `tile-ai/tilelang`
- PR: [1367](https://github.com/tile-ai/tilelang/pull/1367)
- Decision: `Search-matched CUDA kernel optimization PR; materialize diff/source before synthesis.`
- Reason: Search-matched CUDA kernel optimization PR; materialize diff/source before synthesis.

## Changed Paths

- `3rdparty/tvm`
- `CMakeLists.txt`
- `cmake/pypi-z3/FindZ3.cmake`
- `pyproject.toml`
- `requirements-dev.txt`
- `requirements-test.txt`
- `requirements.txt`
- `testing/python/arith/test_arith_hard.py`
- `testing/python/arith/test_arith_intset.py`
- `testing/python/arith/test_arith_iter_affine_map.py`
- `testing/python/arith/test_arith_simplify.py`
- `testing/python/tilelibrary/test_tilelang_tilelibrary_gemm_sp.py`
- `testing/python/transform/test_tilelang_transform_legalize_safe_memory_access.py`
- `tilelang/language/reduce.py`
- `tilelang/utils/sparse.py`

## Evidence Bundle

`evidence/pull-bundles/tilelang/gh-1367`
