z3 z3-5.0.0
Solucionador SMT de alto rendimiento para demostración automática de teoremas, resolución de restricciones y verificación de programas. Soporta múltiples teorías y enlaces de lenguajes para análisis formal.
Z3
Z3 es un demostrador de teoremas de Microsoft Research. Está licenciado bajo la licencia MIT. Las distribuciones binarias de Windows incluyen redistribuibles del runtime de C++
Si no está familiarizado con Z3, puede comenzar aquí.
Los binarios precompilados para versiones estables y nocturnas están disponibles aquí.
Z3 se puede compilar usando [Visual Studio][1], un [Makefile][2], usando [CMake][3], usando [vcpkg][4] o usando [Bazel][5]. Proporciona [enlaces para varios lenguajes de programación][6].
Consulte las notas de la versión para obtener notas sobre varias versiones estables de Z3.
Estado de compilación
Workflows de Pull Request y Push
| Compilación WASM | Compilación Windows | CI | Enlace OCaml |
|---|---|---|---|
 |  |  |  |
Workflows programados
| Errores abiertos | Compilación Android | Rueda Pyodide (PyPI) | Compilación nocturna | Compilación cruzada |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Estático | MSVC Clang-CL | Compilar caché de Z3 | Seguridad de memoria | Marcar PRs listos |
|---|---|---|---|---|
 |  |  |  |  |
Workflows manuales y de lanzamiento
| Documentación | Compilación de lanzamiento | Lanzamiento WASM | Compilación NuGet |
|---|---|---|---|
 |  |  |  |
Workflows especializados
| Validación nocturna | Configuración de Copilot | Mantenimiento de Agentics |
|---|---|---|
 |  |  |
Workflows agentivos
| Coherencia de API | Simplificador de código | Notas de lanzamiento | Sugerencia de workflow | Citación académica |
|---|---|---|---|---|
 |  |  |  |  |