From 7124a07fb71f9f5480278b62523e2e4ccf982226 Mon Sep 17 00:00:00 2001 From: tlopex <820958424@qq.com> Date: Mon, 29 Jun 2026 21:36:22 -0400 Subject: [PATCH] [CI][ARITH] Point CI at the Ubuntu 24.04 images and re-enable USE_Z3 (AUTO) Two related changes, batched because the new CI image is what makes Z3 usable again: 1. Switch CI to the Ubuntu 24.04 (noble) images. Bump ci_tag in ci/jenkins/docker-images.ini to 20260629-192919-24bbfd2e -- the images built from #19893 (ci_cpu/ci_arm/ci_wasm/ci_gpu on Ubuntu 24.04, whose default g++ is gcc-13, giving full C++20 support). 2. Re-enable Z3 (AUTO). #19828 temporarily set USE_Z3=OFF (in CMakeLists.txt and the pyproject wheel build) to dodge a z3-static build failure. The CI image now ships z3-static (#19835), so this restores USE_Z3=AUTO: the Z3-backed Analyzer proving is enabled when z3-static is available and silently skipped otherwise. While Z3 stayed disabled, PrimExprNode::ty became a method, leaving two stale field accesses in z3_prover.cc's IsZ3SupportedExpr (only compiled under TVM_USE_Z3). Fixed expr->ty -> expr->ty(). Verification: - The Ubuntu 24.04 images (#19893) built successfully for ci_cpu/ci_arm/ ci_wasm/ci_gpu (the GPU image includes ROCm 6.4.4 and the CUDA 24.04 base). - Re-enabling Z3 was validated with a build-only wheel run: all four wheels (Linux x86_64/aarch64 manylinux_2_28, macOS arm64, Windows) build green with z3-static compiled and linked, confirming the earlier z3-static link concern is resolved on the current toolchain. --- CMakeLists.txt | 2 +- ci/jenkins/docker-images.ini | 2 +- pyproject.toml | 6 +++--- src/arith/z3_prover.cc | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3d183253b138..567edc1dc698 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -89,7 +89,7 @@ tvm_option(COMPILER_RT_PATH "Path to COMPILER-RT" "3rdparty/compiler-rt") # Contrib library options tvm_option(USE_BLAS "The blas library to be linked" none) tvm_option(USE_AMX "Enable Intel AMX" OFF) -tvm_option(USE_Z3 "Build with Z3 SMT solver support" OFF) +tvm_option(USE_Z3 "Build with Z3 SMT solver support" AUTO) tvm_option(USE_MKL "MKL root path when use MKL blas" OFF) tvm_option(USE_DNNL "Enable DNNL codegen" OFF) tvm_option(USE_CUDNN "Build with cuDNN" OFF) diff --git a/ci/jenkins/docker-images.ini b/ci/jenkins/docker-images.ini index 175ea8dded24..4681ecbc9bcd 100644 --- a/ci/jenkins/docker-images.ini +++ b/ci/jenkins/docker-images.ini @@ -17,7 +17,7 @@ # This data file is read during when Jenkins runs job to determine docker images. [jenkins] -ci_tag: 20260619-214849-4174cdf5 +ci_tag: 20260629-192919-24bbfd2e ci_arm: tlcpack/ci-arm:%(ci_tag)s ci_cpu: tlcpack/ci-cpu:%(ci_tag)s ci_gpu: tlcpack/ci-gpu:%(ci_tag)s diff --git a/pyproject.toml b/pyproject.toml index a4f80182cf11..3e83d4467121 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -16,7 +16,7 @@ # under the License. [build-system] -# z3-static ships the PIC static libz3 + headers for explicit USE_Z3=ON builds. +# z3-static ships the PIC static libz3 + headers consumed by USE_Z3=ON. requires = [ "scikit-build-core>=0.11", "setuptools-scm>=8", @@ -146,8 +146,8 @@ logging.level = "INFO" [tool.scikit-build.cmake.define] TVM_BUILD_PYTHON_MODULE = "ON" USE_CUDA = "OFF" -# Keep Z3 disabled by default until CI's C++ toolchain can link z3-static reliably. -USE_Z3 = "OFF" +# Statically link Z3 from the z3-static build dependency by default. +USE_Z3 = "AUTO" BUILD_TESTING = "OFF" [tool.setuptools_scm] diff --git a/src/arith/z3_prover.cc b/src/arith/z3_prover.cc index 8aa066e2338b..037c47b41dca 100644 --- a/src/arith/z3_prover.cc +++ b/src/arith/z3_prover.cc @@ -556,8 +556,8 @@ class Z3Prover::Impl : ExprFunctor { /// @brief Check if the expression type is supported by z3 integer operations. static bool IsZ3SupportedExpr(const PrimExprNode* expr) { TVM_FFI_DCHECK(expr != nullptr); - TVM_FFI_DCHECK(expr->ty.defined()); - const auto* prim_ty = expr->ty.as(); + TVM_FFI_DCHECK(expr->ty().defined()); + const auto* prim_ty = expr->ty().as(); TVM_FFI_DCHECK(prim_ty != nullptr); return (prim_ty->dtype.code == static_cast(DLDataTypeCode::kDLInt) || prim_ty->dtype.code == static_cast(DLDataTypeCode::kDLUInt) ||