Z3

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

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

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

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

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

Состояние сборки

Azure Pipelines	Code Coverage	Open Bugs	Android Build	WASM Build

Образ Docker.

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

Для 32-битной сборки:

python scripts/mk_make.py

или для 64-битной сборки:

python scripts/mk_make.py -x

затем:

cd build
nmake

Z3 использует C++17. Поэтому рекомендуется использовать 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 имеет несколько зависимостей. Он использует библиотеки времени выполнения C++, включая pthreads для многопоточности. Можно дополнительно использовать GMP для многозначных целых чисел, но Z3 содержит собственную автономную функциональность для работы с многозначными числами. Для сборки Z3 требуется Python. Чтобы собрать Java, .Net, OCaml,