Z3

Z3 — это средство доказательства теорем от Microsoft Research. Оно лицензировано под лицензией MIT. Двоичные дистрибутивы для Windows включают перенаправляемые компоненты среды выполнения C++.

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

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

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

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

Статус сборки

Pull Request & Push Workflows

Scheduled Workflows

Manual & Release Workflows

Specialized Workflows

Nightly Validation	Copilot Setup	Agentics Maintenance

Agentic Workflows

TPTP Benchmark

Сборка 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 или новее.

Функции безопасности (MSVC): При сборке с помощью Visual Studio/MSVC для Z3 по умолчанию включены несколько функций безопасности:

• Control Flow Guard (/guard:cf) — включён по умолчанию для обнаружения попыток скомпрометировать ваш код, предотвращая вызовы в места, отличные от точек входа в функции, что усложняет злоумышленникам выполнение произвольного кода путём перенаправления потока управления
• Address Space Layout Randomization (/DYNAMICBASE) — включён по умолчанию для рандомизации расположения в памяти, требуется параметром компоновщика /GUARD:CF
• Их можно отключить с помощью python scripts/mk_make.py --no-guardcf (сборка через Python) или cmake -DZ3_ENABLE_CFG=OFF (сборка через CMake) при необходимости

Сборка 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 вы можете удалить каталог build и снова запустить скрипт mk_make.py.

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

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

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

vcpkg — это полноценный кроссплатформенный менеджер пакетов. Чтобы установить Z3 с помощью vcpkg, выполните:

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

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

Z3 может быть собран с помощью Bazel. Известно, что это работает на Ubuntu с Clang (но может работать и в других системах с другими компиляторами):

bazel build //...

Зависимости

У самого 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, чтобы включить их сборку.

Инструкции по настройке IDE (Eclipse, IntelliJ IDEA, Visual Studio Code) и устранению неполадок смотрите в Руководстве по настройке Java IDE.

Примеры смотрите в examples/java.

Go

Используйте флаг командной строки --go с mk_make.py, чтобы включить их сборку. Обратите внимание, что привязки Go используют CGO и требуют набора инструментов Go (Go 1.20 или новее) для сборки.

При использовании CMake используйте параметр -DZ3_BUILD_GO_BINDINGS=ON.

Примеры смотрите в examples/go, а полную документацию по API — в src/api/go/README.md.

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) находился в префиксе установки. Если вы используете нестандартный префикс, вы можете использовать параметр --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.

WebAssembly / TypeScript / JavaScript

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

Smalltalk (Pharo / Smalltalk/X)

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

AIX

Настройки сборки для AIX описаны здесь.

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

Интерфейсы

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

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

• C++ API

• .NET API

• Java API

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

• Rust

• C

• OCaml

• Julia

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

Инструменты повышенной функциональности

• Axiom Profiler, в настоящее время разрабатываемый ETH Zurich