z3

Z3

Z3 — средство доказательства теорем от Microsoft Research. Он лицензируется по лицензии MIT.

Если вы не знакомы с Z3, вы можете начать здесь.

Предварительно собранные двоичные файлы для стабильных и ночных выпусков доступны здесь.

Z3 можно собрать с помощью Visual Studio, Makefile или CMake. Он предоставляет привязки для нескольких языков программирования.

См. примечания к выпуску для получения информации о различных стабильных выпусках Z3.

Докер-образ.

Сборка Z3 в Windows с помощью командной строки Visual Studio

32-битные сборки, начните с:

python scripts/mk_make.py

или вместо этого для 64-битной сборки:

python scripts/mk_make.py -x

затем:

 cd build
nmake

Z3 использует C++20. Поэтому рекомендуемой версией Visual Studio является VS2019.

Сборка Z3 с использованием make и GCC/Clang.

Выполнять:

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

Обратите внимание, что по умолчанию в качестве компилятора C++ используется g++ , если он доступен. Если вы предпочитаете использовать Clang, измените вызов mk_make.py на:

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

Обратите внимание, что Clang < 3.7 не поддерживает OpenMP.

Вы также можете собрать Z3 для Windows, используя Cygwin и кросс-компилятор Mingw-w64. Чтобы правильно настроить этот случай, обязательно используйте собственный Python Cygwin, а не какую-либо установку Python для Windows.

Для 64-битной сборки (из Cygwin64) настройте источники Z3 с помощью

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

32-битная сборка должна работать аналогично (но она не тестировалась); то же самое справедливо и для 32/64-битных сборок из Cygwin32.

По умолчанию он устанавливает исполняемый файл z3 в PREFIX/bin , библиотеки в PREFIX/lib и включает файлы в PREFIX/include , где префикс установки PREFIX определяется сценарием mk_make.py . Обычно это /usr для большинства дистрибутивов Linux и /usr/local для FreeBSD и macOS. Используйте параметр командной строки --prefix= чтобы изменить префикс установки. Например:

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

Чтобы удалить Z3, используйте

sudo make uninstall

Чтобы очистить Z3, вы можете удалить каталог сборки и снова запустить скрипт mk_make.py .

Сборка Z3 с использованием CMake

Z3 имеет систему сборки с использованием CMake. Подробности читайте в файле README-CMake.md. Рекомендуется для большинства задач сборки, за исключением создания привязок OCaml.

Сборка Z3 с помощью vcpkg

vcpkg — это полноплатформенный менеджер пакетов, вы можете легко установить libzmq с помощью vcpkg.

Выполнять:

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

Зависимости

Сам Z3 имеет мало зависимостей. Он использует библиотеки времени выполнения C++, включая pthreads для многопоточности. При желании можно использовать GMP для целых чисел с различной точностью, но Z3 содержит свою собственную автономную функциональность с различной точностью. Python необходим для сборки Z3. Для создания API Java, .Net, OCaml, Julia требуется установка соответствующих цепочек инструментов.

Крепления Z3

Z3 имеет привязки для различных языков программирования.

.NET

Вы можете установить пакет nuget для последней версии Z3 с сайта nuget.org.

Используйте флаг командной строки --dotnet с mk_make.py чтобы включить их сборку.

См. examples/dotnet для примеров.

C

Они всегда включены.

См. examples/c .

C++

Они всегда включены.

См. examples/c++ для примеров.

Java

Используйте флаг командной строки --java с mk_make.py чтобы разрешить их сборку.

См. examples/java для примеров.

OCaml

Используйте флаг командной строки --ml с mk_make.py чтобы разрешить их сборку.

См. examples/ml .

Python

Вы можете установить оболочку Python для Z3 для последней версии из pypi с помощью команды:

   pip install z3-solver

Используйте флаг командной строки --python с mk_make.py чтобы разрешить их сборку.

Обратите внимание, что на некоторых платформах требуется, чтобы каталог пакетов Python ( site-packages в большинстве дистрибутивов и dist-packages в дистрибутивах на основе Debian) находился под префиксом install. Если вы используете нестандартный префикс, вы можете использовать опцию --pypkgdir , чтобы изменить каталог пакета Python, используемый для установки. Например:

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

Если вам все же необходимо установить нестандартный префикс, лучшим подходом будет использование виртуальной среды Python и установка Z3 там. Пакеты Python также работают для Python3. В Windows не забудьте выполнить сборку в собственной среде сборки команд Visual C++. Обратите внимание, что каталог build/python/z3 должен быть доступен оттуда, где Python используется с Z3, и это зависит от того, находится ли в пути libz3.dll .

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()) '
...

См. examples/python для примеров.

Julia

Пакет Julia Z3.jl является оболочкой C API Z3. Предыдущая версия включала C++ API: информацию об обновлении и создании привязок Julia можно найти в src/api/julia.

Web Assembly / TypeScript / JavaScript

Сборка WebAssembly со связанными типами TypeScript публикуется на npm как z3-solver. Информацию о создании этих привязок можно найти в src/api/js.

Smalltalk ( Pharo / Smalltalk/X )

Project MachineArithmetic предоставляет интерфейс Smalltalk для C API Z3. Для получения дополнительной информации см. MachineArithmetic/README.md.

Обзор системы

Интерфейсы

• Формат ввода по умолчанию — SMTLIB2.

• Другие собственные интерфейсы внешних функций:

• С++ API

• .NET API

• Java API

• Python API (также доступен в формате pydoc)

• Ржавчина

• С

• OCaml

• Юлия

• Smalltalk (поддерживает Pharo и Smalltalk/X)

Электроинструменты

• Профилировщик Axiom в настоящее время разрабатывается ETH Zurich.