z3prover/z3Solutore SMT ad alte prestazioni per dimostrazione automatica di teoremi, risoluzione di vincoli e verifica di programmi. Supporta molteplici teorie e binding linguistici per l'analisi formale.
Z3 è un dimostratore di teoremi di Microsoft Research. È distribuito sotto la licenza MIT. Le distribuzioni binarie per Windows includono i redistributabili runtime C++
Se non hai familiarità con Z3, puoi iniziare qui.
I binari precompilati per le release stabili e nightly sono disponibili qui.
Z3 può essere compilato usando [CMake][3], [vcpkg][4] o [Bazel][5]. Fornisce [binding per diversi linguaggi di programmazione][6].
Consulta le note di rilascio per informazioni sulle varie release stabili di Z3.
| Build WASM | Build Windows | CI | Binding OCaml |
|---|---|---|---|
 |  |  |  |
| Linter di determinismo | Determinismo del solver |
|---|---|
 |  |
| Build Android | Wheel Pyodide (PyPI) | Build nightly | Build incrociata | Build F* Master |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Sicurezza della memoria | Mark PRs Ready |
|---|---|---|---|---|
 |  |  |  |  |
| Report di avvisi Clang-Tidy |
|---|
 |
| Documentazione | Build di rilascio | Rilascio WASM |
|---|---|---|
 |  |  |
| Validazione nightly | Configurazione Copilot | Manutenzione Agentics | Dispatch NFV Formal Audit |
|---|---|---|---|
 |  |  |  |
| Commento PR del linter di determinismo | Commento PR del determinismo del solver |
|---|---|
 |  |
