This is an automated email from the ASF dual-hosted git repository.
tlopex pushed a commit to branch main
in repository https://gitbox.apache.org/repos/asf/tvm.git
The following commit(s) were added to refs/heads/main by this push:
new f79db0f5a9 [BUILD] Migrate the Z3 dependency to mlc-z3-static (#20084)
f79db0f5a9 is described below
commit f79db0f5a932398fc428d4355a0ccc5986cc12c4
Author: Yixin Dong <[email protected]>
AuthorDate: Mon Aug 3 20:33:16 2026 -0700
[BUILD] Migrate the Z3 dependency to mlc-z3-static (#20084)
## Summary
[mlc-ai/package#110](https://github.com/mlc-ai/package/pull/110) folded
the `z3-static` wheel into `mlc-z3-static` (import module
`mlc_z3_static`; versions restart at 4.16.0 without the `.post1`
suffix). This PR points TVM's Z3 toolchain references at the new
package:
- `cmake/modules/contrib/Z3.cmake` probes `mlc_z3_static.config` first
and keeps the legacy `z3_static.config` probe as a fallback, so existing
environments and the current CI images keep working during the
transition.
- The `pyproject.toml` build requirement becomes
`mlc-z3-static>=4.16.0`.
- The CI docker image installs `mlc-z3-static==4.16.0`.
Note: `mlc-z3-static` is not on PyPI yet. This PR should land only after
the wheel is published; the CMake fallback keeps current CI images
working, but docker image rebuilds and `pyproject.toml`-based wheel
builds need the package on PyPI.
## Verification
Since the wheel is not yet on PyPI, it was built locally from
mlc-ai/package `main` (`254413e`, the #110 merge commit) and its bundled
smoke test passed (static and shared consumers compile, link, and
solve).
- With both `mlc_z3_static` and legacy `z3_static` installed,
`USE_Z3=ON` auto-detection links `mlc_z3_static/static/lib/libz3.a` (new
package preferred).
- With only the legacy `z3-static` package installed, the fallback probe
still finds it.
- Full build against the new package: Z3 statically linked into
`libtvm_compiler.so`, no runtime `libz3` dependency (`ldd`).
- `tests/python/arith/test_arith_z3.py`: 52 passed.
- Full `tests/python/arith/` suite on the same toolchain: 1034 passed, 2
skipped, 26 xfailed.
- `bash -n` on the docker install script passes.
---
cmake/modules/contrib/Z3.cmake | 32 ++++++++++++++-----------
docker/install/ubuntu_install_python_package.sh | 2 +-
pyproject.toml | 6 ++---
3 files changed, 22 insertions(+), 18 deletions(-)
diff --git a/cmake/modules/contrib/Z3.cmake b/cmake/modules/contrib/Z3.cmake
index 5d9af4408f..ec4372bc32 100644
--- a/cmake/modules/contrib/Z3.cmake
+++ b/cmake/modules/contrib/Z3.cmake
@@ -27,25 +27,29 @@ if("${USE_Z3}" MATCHES "^[Aa][Uu][Tt][Oo]$")
set(TVM_Z3_REQUIRED FALSE)
endif()
-# Default lookup: the PIC static Z3 library shipped by the PyPI `z3-static`
+# Default lookup: the PIC static Z3 library shipped by the PyPI `mlc-z3-static`
# package (headers + libz3.a + Z3 CMake package files). Linking it statically
# keeps libtvm free of a runtime libz3 dependency. Users can override the
# lookup by setting Z3_DIR/CMAKE_PREFIX_PATH to any Z3 installation (e.g. a
-# shared system Z3).
+# shared system Z3). The legacy `z3-static` package is still probed as a
+# fallback until environments migrate to `mlc-z3-static`.
if(NOT Z3_DIR)
find_package(Python3 COMPONENTS Interpreter QUIET)
if(Python3_EXECUTABLE)
- execute_process(
- COMMAND
- "${Python3_EXECUTABLE}" -m z3_static.config --cmake-dir
- OUTPUT_VARIABLE Z3_STATIC_CMAKE_DIR
- OUTPUT_STRIP_TRAILING_WHITESPACE
- ERROR_QUIET
- RESULT_VARIABLE Z3_STATIC_RESULT
- )
- if(Z3_STATIC_RESULT EQUAL 0 AND EXISTS "${Z3_STATIC_CMAKE_DIR}")
- set(Z3_DIR "${Z3_STATIC_CMAKE_DIR}")
- endif()
+ foreach(Z3_STATIC_CONFIG_MODULE mlc_z3_static.config z3_static.config)
+ execute_process(
+ COMMAND
+ "${Python3_EXECUTABLE}" -m ${Z3_STATIC_CONFIG_MODULE} --cmake-dir
+ OUTPUT_VARIABLE Z3_STATIC_CMAKE_DIR
+ OUTPUT_STRIP_TRAILING_WHITESPACE
+ ERROR_QUIET
+ RESULT_VARIABLE Z3_STATIC_RESULT
+ )
+ if(Z3_STATIC_RESULT EQUAL 0 AND EXISTS "${Z3_STATIC_CMAKE_DIR}")
+ set(Z3_DIR "${Z3_STATIC_CMAKE_DIR}")
+ break()
+ endif()
+ endforeach()
endif()
endif()
@@ -81,7 +85,7 @@ else()
if(TVM_Z3_REQUIRED)
message(FATAL_ERROR
"USE_Z3 is ON, but Z3 was not found. Install the static Z3 development "
- "package with `pip install 'z3-static>=4.16.0.post1'`, or point "
+ "package with `pip install 'mlc-z3-static>=4.16.0'`, or point "
"Z3_DIR/CMAKE_PREFIX_PATH at a Z3 installation.")
endif()
message(STATUS "Build without Z3 SMT solver support")
diff --git a/docker/install/ubuntu_install_python_package.sh
b/docker/install/ubuntu_install_python_package.sh
index 4445dfd83e..8be4a6a8d7 100755
--- a/docker/install/ubuntu_install_python_package.sh
+++ b/docker/install/ubuntu_install_python_package.sh
@@ -40,4 +40,4 @@ uv pip install --upgrade \
"six~=1.17" \
"tornado~=6.4" \
"ml_dtypes~=0.5" \
- z3-static==4.16.0.post1
+ mlc-z3-static==4.16.0
diff --git a/pyproject.toml b/pyproject.toml
index f7cb27d778..14af7d4c8b 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -16,11 +16,11 @@
# under the License.
[build-system]
-# z3-static ships the PIC static libz3 + headers consumed by USE_Z3=ON.
+# mlc-z3-static ships the PIC static libz3 + headers consumed by USE_Z3=ON.
requires = [
"scikit-build-core>=0.11",
"setuptools-scm>=8",
- "z3-static>=4.16.0.post1",
+ "mlc-z3-static>=4.16.0",
]
build-backend = "scikit_build_core.build"
@@ -146,7 +146,7 @@ logging.level = "INFO"
[tool.scikit-build.cmake.define]
TVM_BUILD_PYTHON_MODULE = "ON"
USE_CUDA = "OFF"
-# Statically link Z3 from the z3-static build dependency by default.
+# Statically link Z3 from the mlc-z3-static build dependency by default.
USE_Z3 = "AUTO"
BUILD_TESTING = "OFF"
