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, un Makefile, usando CMake, usando vcpkg o usando Bazel. Proporciona enlaces para varios lenguajes de programación.

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

Acumulación de issues	Informe de seguridad de memoria	Benchmark QF-S	Analizador de crashes de Specbot	Buscador de benchmarks SMTLIB

Benchmark TPTP

Compilando Z3 en Windows usando el Símbolo del sistema de Visual Studio

Para compilaciones de 32 bits, comience con:

python scripts/mk_make.py

o, en su lugar, para una compilación de 64 bits:

python scripts/mk_make.py -x

luego ejecute:

cd build
nmake

Z3 usa C++20. Por lo tanto, la versión recomendada de Visual Studio es VS2019 o posterior.

Funciones de seguridad (MSVC): Al compilar con Visual Studio/MSVC, un par de funciones de seguridad están habilitadas de forma predeterminada para Z3:

• Guardia de flujo de control (/guard:cf) - habilitada de forma predeterminada para detectar intentos de comprometer su código evitando llamadas a ubicaciones que no sean puntos de entrada de funciones, lo que dificulta que los atacantes ejecuten código arbitrario mediante la redirección del flujo de control
• Aleatorización de diseño del espacio de direcciones (/DYNAMICBASE) - habilitada de forma predeterminada para la aleatorización del diseño de la memoria, requerida por la opción del enlazador /GUARD:CF
• Se pueden deshabilitar usando python scripts/mk_make.py --no-guardcf (compilación con Python) o cmake -DZ3_ENABLE_CFG=OFF (compilación con CMake) si es necesario

Compilando Z3 usando make y GCC/Clang

Ejecute:

python scripts/mk_make.py
cd build
make
sudo make install

Tenga en cuenta que de forma predeterminada se usa g++ como compilador de C++ si está disponible. Si prefiere usar Clang, cambie la invocación de mk_make.py a:

CXX=clang++ CC=clang python scripts/mk_make.py

Tenga en cuenta que Clang < 3.7 no admite OpenMP.

También puede compilar Z3 para Windows usando Cygwin y el compilador cruzado Mingw-w64. En ese caso, asegúrese de usar el Python propio de Cygwin y no alguna instalación de Python de Windows.

Para una compilación de 64 bits (desde Cygwin64), configure las fuentes de Z3 con

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

Una compilación de 32 bits debería funcionar de manera similar (pero no está probada); lo mismo es cierto para compilaciones de 32/64 bits desde Cygwin32.

De forma predeterminada, instalará los ejecutables de z3 en PREFIX/bin, las bibliotecas en PREFIX/lib y los archivos de inclusión en PREFIX/include, donde el prefijo de instalación PREFIX lo infiere el script mk_make.py. Por lo general, es /usr para la mayoría de las distribuciones de Linux y /usr/local para FreeBSD y macOS. Use la opción de línea de comandos --prefix= para cambiar el prefijo de instalación. Por ejemplo:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

Para desinstalar Z3, use

sudo make uninstall

Para limpiar Z3, puede eliminar el directorio de compilación y ejecutar el script mk_make.py nuevamente.

Compilando Z3 usando CMake

Z3 tiene un sistema de compilación que usa CMake. Lea el archivo README-CMake.md para obtener más detalles. Se recomienda para la mayoría de las tareas de compilación, excepto para compilar enlaces OCaml.

Compilando Z3 usando vcpkg

vcpkg es un administrador de paquetes multiplataforma completo. Para instalar Z3 con vcpkg, ejecute:

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Compilando Z3 usando Bazel

Z3 se puede compilar usando Bazel. Se sabe que funciona en Ubuntu con Clang (pero puede funcionar en otros lugares con otros compiladores):

bazel build //...

Dependencias

Z3 en sí tiene pocas dependencias. Utiliza bibliotecas de tiempo de ejecución de C++, incluyendo pthreads para subprocesamiento múltiple. Opcionalmente, es posible usar GMP para enteros de precisión múltiple, pero Z3 contiene su propia funcionalidad de precisión múltiple autónoma. Se requiere Python para compilar Z3. La compilación de las API de Java, .NET, OCaml y Julia requiere instalar las cadenas de herramientas correspondientes.

Enlaces de Z3

Z3 tiene enlaces para varios lenguajes de programación.

.NET

Puede instalar un paquete NuGet para la última versión de Z3 desde nuget.org.

Use la bandera de línea de comandos --dotnet con mk_make.py para habilitar la compilación de estos.

Consulte examples/dotnet para ver ejemplos.

C

Estos están siempre habilitados.

Consulte examples/c para ver ejemplos.

C++

Estos están siempre habilitados.

Consulte examples/c++ para ver ejemplos.

Java

Use la bandera de línea de comandos --java con mk_make.py para habilitar la compilación de estos.

Para instrucciones de configuración de IDE (Eclipse, IntelliJ IDEA, Visual Studio Code) y solución de problemas, consulte la Guía de configuración de IDE para Java.

Consulte examples/java para ver ejemplos.

Go

Use la bandera de línea de comandos --go con mk_make.py para habilitar la compilación de estos. Tenga en cuenta que los enlaces de Go usan CGO y requieren una cadena de herramientas de Go (Go 1.20 o posterior) para compilar.

Con CMake, use la opción -DZ3_BUILD_GO_BINDINGS=ON.

Consulte examples/go para ver ejemplos y src/api/go/README.md para obtener la documentación completa de la API.

OCaml

Use la bandera de línea de comandos --ml con mk_make.py para habilitar la compilación de estos.

Consulte examples/ml para ver ejemplos.

Python

Puede instalar el envoltorio de Python para Z3 para la última versión desde pypi usando el comando:

   pip install z3-solver

Use la bandera de línea de comandos --python con mk_make.py para habilitar la compilación de estos.

Tenga en cuenta que en ciertas plataformas se requiere que el directorio del paquete de Python (site-packages en la mayoría de las distribuciones y dist-packages en distribuciones basadas en Debian) esté dentro del prefijo de instalación. Si usa un prefijo no estándar, puede usar la opción --pypkgdir para cambiar el directorio del paquete de Python utilizado para la instalación. Por ejemplo:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

Si necesita instalar en un prefijo no estándar, un mejor enfoque es usar un entorno virtual de Python e instalar Z3 allí. Los paquetes de Python también funcionan para Python3. En Windows, recuerde compilar dentro del entorno de compilación de comandos nativos de Visual C++. Tenga en cuenta que el directorio build/python/z3 debe ser accesible desde donde se use Python con Z3 y requiere que libz3.dll esté en la ruta.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# Encontrará Z3 y los enlaces de Python instalados en el entorno virtual
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

Consulte examples/python para ver ejemplos.

Julia

El paquete de Julia Z3.jl envuelve la API de C de Z3. Una versión anterior lo envolvía con la API de C++: la información sobre la actualización y compilación de los enlaces de Julia se puede encontrar en src/api/julia.

WebAssembly / TypeScript / JavaScript

Una compilación de WebAssembly con tipificaciones de TypeScript asociadas se publica en npm como z3-solver. La información sobre la compilación de estos enlaces se puede encontrar en src/api/js.

Smalltalk (Pharo / Smalltalk/X)

El proyecto MachineArithmetic proporciona una interfaz de Smalltalk para la API de C de Z3. Para obtener más información, consulte MachineArithmetic/README.md.

AIX

La configuración de compilación para AIX se describe aquí.

Descripción general del sistema

Interfaces

• El formato de entrada predeterminado es SMTLIB2

• Otras interfaces nativas de funciones externas:

• API de C++

• API de .NET

• API de Java

• API de Python (también disponible en formato pydoc)

• Rust

• C

• OCaml

• Julia

• Smalltalk (admite Pharo y Smalltalk/X)

Herramientas avanzadas

• El Axiom Profiler actualmente desarrollado por ETH Zurich