Descarga z3 - Descarga del código fuente z3

z3

Otro código fuente

z3-4.13.3

Descargar

Z3

Z3 es un demostrador de teoremas de Microsoft Research. Tiene licencia bajo la licencia MIT.

Si no estás familiarizado con el Z3, puedes empezar aquí.

Los archivos binarios prediseñados para lanzamientos estables y nocturnos están disponibles desde aquí.

Z3 se puede construir usando Visual Studio, un Makefile o usando CMake. Proporciona enlaces para varios lenguajes de programación.

Consulte las notas de la versión para obtener notas sobre varias versiones estables de Z3.

Imagen acoplable.

Construyendo Z3 en Windows usando el símbolo del sistema de Visual Studio

Construcciones 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

entonces:

 cd build
nmake

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

Construyendo Z3 usando make y GCC/Clang

Ejecutar:

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

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

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

Tenga en cuenta que Clang < 3.7 no es compatible con OpenMP.

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

Para una compilación de 64 bits (de 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 ocurre con las compilaciones de 32/64 bits desde Cygwin32.

De forma predeterminada, instalará el ejecutable z3 en PREFIX/bin , las bibliotecas en PREFIX/lib e incluirá archivos en PREFIX/include , donde el script mk_make.py infiere el prefijo de instalación PREFIX . Suele ser /usr para la mayoría de las distribuciones de Linux y /usr/local para FreeBSD y macOS. Utilice la opción de línea de comando --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.

Construyendo Z3 usando CMake

Z3 tiene un sistema de compilación que utiliza 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 la creación de enlaces OCaml.

Construyendo Z3 usando vcpkg

vcpkg es un administrador de paquetes de plataforma completa; puede instalar libzmq fácilmente con vcpkg.

Ejecutar:

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

Dependencias

El propio Z3 tiene pocas dependencias. Utiliza bibliotecas de tiempo de ejecución de C++, incluidos pthreads para subprocesos múltiples. Opcionalmente, es posible utilizar GMP para números enteros de precisión múltiple, pero Z3 contiene su propia funcionalidad de precisión múltiple autónoma. Se requiere Python para construir Z3. Para crear las API de Java, .Net, OCaml y Julia es necesario instalar cadenas de herramientas relevantes.

fijaciones Z3

Z3 tiene enlaces para varios lenguajes de programación.

`.NET`

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

Utilice la marca de línea de comando --dotnet con mk_make.py para permitir su construcción.

Consulte examples/dotnet para ver ejemplos.

`C`

Estos siempre están habilitados.

Ver examples/c para ejemplos.

`C++`

Estos siempre están habilitados.

Consulte examples/c++ para ver ejemplos.

`Java`

Utilice el indicador de línea de comando --java con mk_make.py para permitir su construcción.

Consulte examples/java para ver ejemplos.

`OCaml`

Utilice el indicador de línea de comando --ml con mk_make.py para permitir su construcción.

Ver examples/ml para ejemplos.

`Python`

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

   pip install z3-solver

Utilice el indicador de línea de comando --python con mk_make.py para permitir su construcción.

Tenga en cuenta que en ciertas plataformas se requiere que el directorio de paquetes de Python ( site-packages en la mayoría de las distribuciones y dist-packages en distribuciones basadas en Debian) se encuentre bajo el prefijo de instalación. Si usa un prefijo no estándar, puede usar la opción --pypkgdir para cambiar el directorio del paquete Python usado 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 con un prefijo no estándar, un mejor enfoque es utilizar un entorno virtual 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 nativo de Visual C++. Tenga en cuenta que se debe poder acceder al directorio build/python/z3 desde donde se usa Python con Z3 y depende de que libz3.dll esté en la ruta.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c ' import z3; print(z3.get_version_string()) '
...

Consulte examples/python para ver ejemplos.

`Julia`

El paquete Julia Z3.jl envuelve la API C de Z3. Una versión anterior incluía la API de C++: la información sobre cómo actualizar y crear los enlaces de Julia se puede encontrar en src/api/julia.

`Web Assembly` / `TypeScript` / `JavaScript`

Una compilación de WebAssembly con tipos de TypeScript asociados se publica en npm como z3-solver. Puede encontrar información sobre la creación de estos enlaces en src/api/js.