Ubospica opened a new pull request, #19667:
URL: https://github.com/apache/tvm/pull/19667
# [ARITH] Add optional Z3-backed proving to Analyzer
## Summary
This PR adds an optional Z3 SMT solver backend to `tvm::arith::Analyzer` for
stronger integer arithmetic proving.
The integration is disabled by default and guarded by a new `USE_Z3` CMake
option. When enabled, `Analyzer::CanProve` keeps the existing TVM arithmetic
analysis path first, then falls back to Z3 only when the existing analyzers
cannot prove the predicate. When disabled, a stub implementation is built so
the C++ and Python APIs remain available without requiring Z3.
## Features
This PR adds:
- Optional Z3 build support through `USE_Z3`, defaulting to `OFF`.
- A new `arith::Z3Prover` sub-analyzer owned by `arith::Analyzer`.
- Updated `Analyzer::CanProve` flow: it first runs the existing TVM logic
(simplify, const-int-bound, int-set, transitive comparison) unchanged; only if
that fails does it ask `z3_prover.CanProve(simplified)`, which proves the
predicate by checking that its negation is unsatisfiable under the current
constraints. Z3 is a pure fallback and a negative/unknown result keeps the
original `false`.
- SMT-LIB2 export for debugging and external solver reproduction.
- Python APIs:
- `Analyzer.get_smtlib2(expr=None)`
- `Analyzer.set_z3_timeout_ms(timeout_ms)`
- `Analyzer.set_z3_rlimit(rlimit)`
- `Analyzer.get_z3_stats()`
- C++ APIs:
- `Z3Prover::CanProve`
- `Z3Prover::Bind`
- `Z3Prover::EnterConstraint`
- `Z3Prover::GetSMTLIB2`
- `Z3Prover::GetStats`
- `Z3Prover::SetTimeoutMs`
- `Z3Prover::SetRLimit`
- `Z3Prover::GetModel`
- `Z3Prover::CountSatisfyingValues`
- Scalar integer, unsigned integer, and boolean expression translation to Z3.
- Support for arithmetic, comparisons, boolean operators, `min`, `max`,
`select`, `let`, casts, floor division, floor 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.
## TileLang References
The implementation is based on the Z3 analyzer integration used in
TileLang's TVM fork, with the upstream port kept optional and scoped to TVM's
arithmetic analyzer.
- [tile-ai/tilelang#1367](https://github.com/tile-ai/tilelang/pull/1367)
- [tile-ai/tilelang#1458](https://github.com/tile-ai/tilelang/pull/1458)
- [tile-ai/tilelang#2216](https://github.com/tile-ai/tilelang/pull/2216)
- [TileLang/tvm#22](https://github.com/TileLang/tvm/pull/22)
- [TileLang/tvm#24](https://github.com/TileLang/tvm/pull/24)
## Differences From TileLang
The core `Z3Prover` algorithm is kept close to the latest TileLang TVM
implementation. The differences are in how it is integrated into upstream TVM:
1. **Optional build.** We make Z3 optional, defaulting `USE_Z3=OFF` and
building a `z3_prover_off.cc` stub when disabled, so Z3 stays out of the
default build. In TileLang it is enabled by default.
2. **Z3 discovery.** We add `cmake/modules/contrib/Z3.cmake`, which prefers
a system Z3 and falls back to the PyPI `z3-solver` package. TileLang resolves
Z3 from `z3-solver` directly.
3. **`is_assume` propagation.** We forward `is_assume` from
`Analyzer::EnterConstraint` into the Z3 prover so it handles assumption scopes
the same way as the rewrite simplifier. The previous implementation in TileLang
does not forward this flag.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
