diff --git a/cmake/modules/contrib/Z3.cmake b/cmake/modules/contrib/Z3.cmake index 5d9af4408fb6..ec4372bc322e 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 4445dfd83eb1..8be4a6a8d7ab 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 f7cb27d778dc..14af7d4c8b05 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"