Z3

Z3 は、Microsoft Research の定理証明器です。 MIT ライセンスの下で提供されています。Windows バイナリ配布には C++ ランタイム再頒布可能パッケージが含まれています。

Z3 に詳しくない場合は、こちらから始めることができます。

安定版およびナイトリーリリースのプリビルドバイナリはこちらから入手できます。

Z3 は、Visual Studio、Makefile、CMake、vcpkg、または Bazel を使用してビルドできます。また、いくつかのプログラミング言語向けのバインディングを提供しています。

各種安定版リリースに関する注意事項については、リリースノートを参照してください。

ビルドステータス

プルリクエスト & プッシュワークフロー

WASM ビルド	Windows ビルド	CI	OCaml バインディング

定期実行ワークフロー

Open Bugs	Android ビルド	Pyodide Wheel (PyPI)	ナイトリービルド	クロスビルド

MSVC スタティック	MSVC Clang-CL	Z3 キャッシュのビルド	メモリ安全性	PR のレビュー準備完了

手動 & リリースワークフロー

ドキュメント	リリースビルド	WASM リリース	NuGet ビルド

特化ワークフロー

ナイトリー検証	Copilot セットアップ	Agentics メンテナンス

エージェンティックワークフロー

API 一貫性	コード簡略化	リリースノート	ワークフロー提案	学術引用

課題バックログ	メモリ安全性レポート	QF-S ベンチマーク	Specbot クラッシュアナライザ	SMTLIB ベンチマークファインダー

TPTP ベンチマーク

Visual Studio コマンドプロンプトを使用した Windows での Z3 のビルド

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 ではデフォルトでいくつかのセキュリティ機能が有効になっています。

コントロールフローガード (/guard:cf) - 関数エントリポイント以外の場所への呼び出しを防止することで、コードへの不正アクセス試行を検出し、攻撃者が制御フローのリダイレクトを通じて任意のコードを実行することをより困難にします。
アドレス空間レイアウトのランダム化 (/DYNAMICBASE) - メモリレイアウトのランダム化のためにデフォルトで有効になっており、/GUARD:CF リンカーオプションに必要です。
これらは、必要に応じて python scripts/mk_make.py --no-guardcf (Python ビルド) または cmake -DZ3_ENABLE_CFG=OFF (CMake ビルド) を使用して無効にすることができます。

make と GCC/Clang を使用した Z3 のビルド

以下を実行します。

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

デフォルトでは、g++ が利用可能であれば、C++ コンパイラとして使用されます。 Clang を使用したい場合は、mk_make.py の呼び出しを次のように変更します。

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

Clang < 3.7 は OpenMP をサポートしていないことに注意してください。

また、Cygwin と Mingw-w64 クロスコンパイラを使用して、Windows 向けに Z3 をビルドすることもできます。その場合、Cygwin 自身の Python を使用し、Windows にインストールされた Python は使用しないようにしてください。

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 ビットビルドも同様に動作するはずですが (未テスト)、Cygwin32 からの 32/64 ビットビルドについても同様です。

デフォルトでは、z3 実行ファイルは PREFIX/bin に、ライブラリは PREFIX/lib に、インクルードファイルは PREFIX/include にインストールされます。ここで PREFIX インストールプレフィックスは mk_make.py スクリプトによって推測されます。ほとんどの Linux ディストリビューションでは通常 /usr であり、FreeBSD と macOS では /usr/local です。インストールプレフィックスを変更するには、--prefix= コマンドラインオプションを使用します。例：

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

Z3 をアンインストールするには、次を使用します。

sudo make uninstall

Z3 をクリーンするには、ビルドディレクトリを削除し、mk_make.py スクリプトを再度実行します。

CMake を使用した Z3 のビルド

Z3 には CMake を使用したビルドシステムがあります。詳細については README-CMake.md ファイルを参照してください。OCaml バインディングのビルドを除くほとんどのビルドタスクに推奨されます。

vcpkg を使用した Z3 のビルド

vcpkg は完全なプラットフォームパッケージマネージャーです。vcpkg で Z3 をインストールするには、以下を実行します。

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # PowerShell の場合
./bootstrap-vcpkg.sh # bash の場合
./vcpkg install z3

Bazel を使用した Z3 のビルド

Z3 は Bazel を使用してビルドできます。これは Ubuntu で Clang を使用して動作することが確認されています (他の環境でも他のコンパイラで動作する可能性があります)：

bazel build //...

依存関係

Z3 自体の依存関係は非常に少ないです。C++ ランタイムライブラリを使用し、マルチスレッド化には pthreads を含みます。オプションで GMP を多倍長整数に使用することも可能ですが、Z3 には自己完結型の多倍長機能が含まれています。Z3 をビルドするには Python が必要です。Java、.NET、OCaml、Julia API のビルドには、関連するツールチェーンのインストールが必要です。

Z3 バインディング

Z3 には様々なプログラミング言語向けのバインディングがあります。

`.NET`

最新リリースの Z3 の NuGet パッケージは nuget.org からインストールできます。

mk_make.py で --dotnet コマンドラインフラグを使用すると、これらのビルドが有効になります。

例については examples/dotnet を参照してください。

`C`

これらは常に有効です。

例については examples/c を参照してください。

`C++`

これらは常に有効です。

例については examples/c++ を参照してください。

`Java`

mk_make.py で --java コマンドラインフラグを使用すると、これらのビルドが有効になります。

IDE (Eclipse、IntelliJ IDEA、Visual Studio Code) のセットアップ手順とトラブルシューティングについては、Java IDE セットアップガイドを参照してください。

例については examples/java を参照してください。

`Go`

mk_make.py で --go コマンドラインフラグを使用すると、これらのビルドが有効になります。Go バインディングは CGO を使用しており、ビルドには Go ツールチェーン (Go 1.20 以降) が必要です。

CMake を使用する場合は、-DZ3_BUILD_GO_BINDINGS=ON オプションを使用します。

例については examples/go を、完全な API ドキュメントについては src/api/go/README.md を参照してください。

`OCaml`

mk_make.py で --ml コマンドラインフラグを使用すると、これらのビルドが有効になります。

例については examples/ml を参照してください。

`Python`

最新リリースの Z3 用 Python ラッパーは、pypi から次のコマンドでインストールできます。

   pip install z3-solver

mk_make.py で --python コマンドラインフラグを使用すると、これらのビルドが有効になります。

特定のプラットフォームでは、Python パッケージディレクトリ (ほとんどのディストリビューションでは site-packages、Debian ベースのディストリビューションでは dist-packages) がインストールプレフィックスの下にある必要があることに注意してください。非標準のプレフィックスを使用する場合は、--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 ディレクトリは、Z3 で Python を使用する場所からアクセス可能であり、パスに libz3.dll が必要であることに注意してください。

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# 仮想環境に Z3 と Python バインディングがインストールされていることがわかります
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

例については examples/python を参照してください。

`Julia`

Julia パッケージ Z3.jl は Z3 の C API をラップしています。以前のバージョンでは C++ API をラップしていました。Julia バインディングの更新とビルドに関する情報は src/api/julia にあります。

`WebAssembly` / `TypeScript` / `JavaScript`

関連する TypeScript 型定義を含む WebAssembly ビルドは、npm に z3-solver として公開されています。これらのバインディングのビルドに関する情報は src/api/js にあります。

Smalltalk (`Pharo` / `Smalltalk/X`)

プロジェクト MachineArithmetic は、Z3 の C API への Smalltalk インターフェースを提供しています。詳細については、MachineArithmetic/README.md を参照してください。

AIX

AIX のビルド設定はこちらに説明されています。

システム概要

System Diagram

インターフェース

デフォルトの入力形式は SMTLIB2 です。
その他のネイティブ外部関数インターフェース：
C++ API
.NET API
Java API
Python API (pydoc 形式でも利用可能)
Rust
C
OCaml
Julia
Smalltalk (Pharo と Smalltalk/X をサポート)

パワーツール

Axiom Profiler は現在 ETH Zurich によって開発されています

z3 z3-5.0.0

カテゴリ