[Bugfix] Add bv2int & int2bv for not & shift operation in z3#24
Merged
silentCoder-dev merged 1 commit intoJan 12, 2026
Merged
Conversation
This was referenced Jun 3, 2026
tlopex
pushed a commit
to apache/tvm
that referenced
this pull request
Jun 18, 2026
## Summary This PR adds a Z3 SMT solver backend to `tvm::arith::Analyzer` for stronger integer arithmetic proving. The integration is guarded by `USE_Z3`, which defaults to `AUTO`. In the default mode, TVM enables Z3 when the static Z3 development artifacts are available and otherwise builds the conservative stub implementation. When Z3 is enabled, `Analyzer::CanProve` runs the existing TVM arithmetic analysis path first, then falls back to Z3 only when the existing analyzers cannot prove the predicate and the requested strength is `kSymbolicBound`. Z3 is linked statically from the PyPI `z3-static` package, so `libtvm` does not need a runtime `libz3` dependency. ## Features - Z3 build support through `USE_Z3`, defaulting to `AUTO`. - A new `arith::Z3Prover` sub-analyzer owned by `arith::Analyzer`. - SMT-LIB2 export for debugging and external solver reproduction. - Python debug/config APIs: `Analyzer.get_smtlib2`, `Analyzer.set_z3_timeout_ms`, `Analyzer.set_z3_rlimit`, and `Analyzer.get_z3_stats`. - C++ APIs for proving, binding, constraints, stats, model inspection, and satisfying-value counting. - Scalar integer, unsigned integer, and boolean expression translation to Z3. - Support for arithmetic, comparisons, boolean operators, `min`, `max`, `select`, `if_then_else`, `let`, casts, truncated division/modulo, floor division/modulo, and selected bitwise/shift operations. - Deterministic solver control using Z3 `rlimit`, with `random_seed` fixed to `42`. - Thread-local Z3 context sharing to reduce initialization overhead while keeping thread safety. - A disabled-mode stub implementation that returns conservative results when Z3 is not built. ## Implementation Notes - The real and stub implementations live in `src/arith/z3_prover.cc`, selected by the `TVM_USE_Z3` macro from `cmake/modules/contrib/Z3.cmake`. - `cmake/modules/contrib/Z3.cmake` first resolves the PIC static `libz3` layout provided by `z3-static` using its `z3_static.get_cmake_dir()` helper, then falls back to a custom `Z3_DIR` or `CMAKE_PREFIX_PATH` installation. - `USE_Z3=ON` requires Z3 to be found, while `USE_Z3=AUTO` allows source builds and CI jobs without Z3 artifacts to continue with the stub. - The Z3 fallback is exception-safe and gated behind `kSymbolicBound`, so the common `kDefault` path does not pay solver cost. - TVM `Div` and `Mod` are translated with truncating helpers rather than Z3's Euclidean operators to stay sound for negative dividends. - Shift handling relies on Z3's native bit-vector semantics and does not add hard assertions to the shared solver. ## References The implementation is based on the Z3 analyzer integration used in TileLang's TVM fork, with the upstream port kept scoped to TVM's arithmetic analyzer. - [tile-ai/tilelang#1367](tile-ai/tilelang#1367) - [tile-ai/tilelang#1458](tile-ai/tilelang#1458) - [tile-ai/tilelang#2216](tile-ai/tilelang#2216) - [tile-ai#22](tile-ai#22) - [tile-ai#24](tile-ai#24) - [Original TileLang TVM commit](tile-ai@e633295) --------- Signed-off-by: Ubospica <ubospica@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.