# Z3 Z3 は Microsoft Research による定理証明器です。 [MIT ライセンス](https://github.com/z3prover/z3/blob/master/LICENSE.txt)の下でライセンスされています。Windows 用バイナリ配布物には [C++ ランタイム再頒布可能パッケージ](https://visualstudio.microsoft.com/license-terms/vs2022-cruntime/)が含まれています。 Z3 に馴染みがない場合は、[こちら](https://github.com/Z3Prover/z3/wiki#background)から始めることができます。 安定版およびナイトリリースのビルド済みバイナリは[こちら](https://github.com/Z3Prover/z3/releases)で入手できます。 Z3 は [CMake][3]、[vcpkg][4]、または [Bazel][5] を使用してビルドできます。 [複数のプログラミング言語向けのバインディング][6]を提供しています。 Z3 の各種安定版リリースに関する注意事項については、[リリースノート](https://github.com/z3prover/z3/blob/master/RELEASE_NOTES.md)を参照してください。 [](https://microsoft.github.io/z3guide/) ## ビルドステータス ### プルリクエストおよびプッシュのワークフロー | WASM ビルド | Windows ビルド | CI | 有限体リグレッション | | ------------|---------------|----------------------|-------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ci.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/finite-field.yml) | | 決定性リンター | ソルバーの決定性 | Pulse ネイティブチェッカーのビルド | |---------------------|---------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-report.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-build.yml) | ### スケジュールされたワークフロー | Android ビルド | ナイトリービルド | クロスビルド | F* マスタービルド | | ---------------|---------------|-------------|------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nightly.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/cross-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml) | | MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready | |-------------|---------------|----------------|---------------|----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build-clang-cl.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/build-z3-cache.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/mark-prs-ready-for-review.yml) | | Clang-Tidy Warning Report | |----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/clang-tidy-warning-report.yml) | ### 手動およびリリースワークフロー | Documentation | Release Build | WASM Release | Pyodide Wheel (PyPI) | |---------------|---------------|--------------|---------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/docs.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wasm-release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide-pypi.yml) | ### 特化ワークフロー | Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit | |--------------------|---------------|----------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/nightly-validation.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/copilot-setup-steps.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/agentics-maintenance.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nfv-formal-audit-dispatcher.yml) | ### フォローアップ / コメントワークフロー | Determinism Linter PR Comment | Solver Determinism PR Comment | Pulse Checker Regressions | |--------------------------------|---------------------------------|--------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-regressions.yml) | ### エージェント型ワークフロー | API整合性 | コード簡素化 | リリースノート | ワークフロー提案 | 学術引用 | | -------------|-----------------|---------------|---------------------|-------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/api-coherence-checker.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-simplifier.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release-notes-updater.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/workflow-suggestion-agent.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/academic-citation-tracker.lock.yml) | | イシューバックログ | メモリ安全性レポート | SMTLIBベンチマーク検索 | F* NFV PR監査 | | --------------|----------------------|-------------------------|-----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/issue-backlog-processor.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety-report.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/smtlib-benchmark-finder.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-nfv-audit.lock.yml) | | A3 Python解析 | コード規約 | 統計比較異常レポーター | CSA解析 | タクティックから簡素化へ | |----------------------|-------------------|----------------------------------|----------------|------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/a3-python.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-conventions-analyzer.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/compare-stats-anomaly-reporter.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/csa-analysis.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/tactic-to-simplifier.lock.yml) | [3]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-cmake [4]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-vcpkg [5]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-bazel [6]: https://raw.githubusercontent.com/z3prover/z3/master/#z3-bindings ## CMakeを使用したZ3のビルド CMakeはZ3にとって推奨される、最も機能が充実したビルドシステムです。基本的な リリースビルドは以下の通りです。 ```bash cmake -S . -B build -DCMAKE_BUILD_TYPE=Release cmake --build build --parallel $(nproc) ``` ビルドオプション、言語バインディング、インストール、および別の CMake プロジェクトから Z3 を利用する方法については、[README-CMake.md](https://github.com/z3prover/z3/blob/master/README-CMake.md) を参照してください。 Z3 は C++20 を使用します。そのため Windows では、推奨される Visual Studio のバージョンは VS2019 以降です。CMake を Ninja または Visual Studio ジェネレーターと共に使用すると、Visual Studio コマンドプロンプトから Z3 をビルドできます。 **セキュリティ機能 (MSVC)**: Visual Studio/MSVC でビルドする場合、Z3 ではいくつかのセキュリティ機能がデフォルトで有効になります: - 制御フローガード (`/guard:cf`) - 関数のエントリポイント以外への呼び出しを防ぐことでコードを侵害しようとする試みを検出するため、デフォルトで有効になります。これにより、攻撃者が制御フローのリダイレクトを通じて任意のコードを実行することがより困難になります - アドレス空間配置のランダム化 (`/DYNAMICBASE`) - メモリレイアウトのランダム化のためにデフォルトで有効になり、`/GUARD:CF` リンカーオプションで必要とされます - 必要に応じて `cmake -S . -B build -DZ3_ENABLE_CFG=OFF` を使用してこれらを無効にできます システムのプレフィックスにインストールするには `sudo cmake --install build` を使用します (カスタムプレフィックスの場合は構成時に `-DCMAKE_INSTALL_PREFIX=` を設定します)。アンインストールするには、お使いのプラットフォームのパッケージマネージャーを参照するか、CMake がインストールされたファイルを `build/install_manifest.txt` に記録しているため、それらのファイルを直接削除してください。 ## vcpkg を使用した Z3 のビルド vcpkg は完全なプラットフォームパッケージマネージャーです。vcpkg で Z3 をインストールするには、次を実行します: ```bash git clone https://github.com/microsoft/vcpkg.git ./bootstrap-vcpkg.bat # For powershell ./bootstrap-vcpkg.sh # For bash ./vcpkg install z3 ``` ## Bazel を使用した Z3 のビルド Z3 は [Bazel](https://bazel.build/) を使用してビルドできます。これは Clang を使用した Ubuntu で動作することが確認されています（他の環境や他のコンパイラでも動作する可能性があります）： ``` bazel build //... ``` ## 依存関係 Z3 自体の依存関係はごくわずかです。マルチスレッド用の pthreads を含む C++ ランタイムライブラリを使用します。 オプションで多倍長整数に GMP を使用することも可能ですが、Z3 には自己完結型の 多倍長演算機能が含まれています。Z3 のビルドには Python が必要です。Java、.NET、OCaml、および Julia API のビルドには、関連するツールチェーンのインストールが必要です。 ## Z3 バインディング Z3 にはさまざまなプログラミング言語向けのバインディングがあります。 ### ``.NET`` 最新リリースの Z3 用 NuGet パッケージを [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/) からインストールできます。 CMake では、``-DZ3_BUILD_DOTNET_BINDINGS=ON`` オプションを使用します。 例については [``examples/dotnet``](https://github.com/z3prover/z3/blob/master/examples/dotnet) を参照してください。 ### ``C`` これらは常に有効です。 例については [``examples/c``](https://github.com/z3prover/z3/blob/master/examples/c) を参照してください。 ### ``C++`` これらは常に有効です。 例については [``examples/c++``](https://github.com/z3prover/z3/blob/master/examples/c%2B%2B) を参照してください。 ### ``Java`` CMake では、``-DZ3_BUILD_JAVA_BINDINGS=ON`` オプションを使用します。 IDE のセットアップ手順（Eclipse、IntelliJ IDEA、Visual Studio Code）とトラブルシューティングについては、[Java IDE セットアップガイド](https://github.com/z3prover/z3/blob/master/doc/JAVA_IDE_SETUP.md)を参照してください。 例については [``examples/java``](https://github.com/z3prover/z3/blob/master/examples/java) を参照してください。 ### ``Go`` CMake では、``-DZ3_BUILD_GO_BINDINGS=ON`` オプションを使用します。Go バインディングは CGO を使用し、ビルドには Go ツールチェーン（Go 1.20 以降）が必要であることに注意してください。 例については [``examples/go``](https://github.com/z3prover/z3/blob/master/examples/go) を、完全な API ドキュメントについては [``src/api/go/README.md``](https://github.com/z3prover/z3/blob/master/src/api/go/README.md) を参照してください。 ### ``OCaml`` CMake では、``-DZ3_BUILD_OCAML_BINDINGS=ON`` オプションを使用します。 例については [``examples/ml``](https://github.com/z3prover/z3/blob/master/examples/ml) を参照してください。 ### ``Python`` 最新リリースの Z3 用 Python ラッパーは、次のコマンドを使用して pypi からインストールできます: ```bash pip install z3-solver ``` CMake を使用する場合は、``-DZ3_BUILD_PYTHON_BINDINGS=ON`` オプションを使用してください。 一部のプラットフォームでは、Python パッケージディレクトリ（ほとんどのディストリビューションでは ``site-packages``、Debian ベースのディストリビューションでは ``dist-packages``）がインストールプレフィックスの下に存在することが必要であることに注意してください。非標準のプレフィックスを使用する場合は、``-DCMAKE_INSTALL_PYTHON_PKG_DIR=`` オプションを使用して、インストールに使用する Python パッケージディレクトリを変更できます。例: ```bash cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/home/leo -DZ3_BUILD_PYTHON_BINDINGS=ON -DCMAKE_INSTALL_PYTHON_PKG_DIR=/home/leo/lib/python3.x/site-packages ``` 非標準のプレフィックスにインストールする必要がある場合は、[Python仮想環境](https://virtualenv.readthedocs.org/en/latest/)を使用してそこにZ3をインストールする方が良い方法です。 Windowsでは、Visual C++ネイティブコマンドビルド環境内でビルドすることを忘れないでください。 ``build/python/z3``ディレクトリは、Z3と共にPythonが使用される場所からアクセス可能である必要があり、 ``libz3.dll``がパス内にあることが必要です。 ```bash virtualenv venv source venv/bin/activate cmake -S . -B build -DCMAKE_INSTALL_PREFIX=$VIRTUAL_ENV -DZ3_BUILD_PYTHON_BINDINGS=ON cmake --build build --parallel $(nproc) cmake --install build # 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``](https://github.com/z3prover/z3/blob/master/examples/python)を参照してください。 ### ``Julia`` Juliaパッケージ[Z3.jl](https://github.com/ahumenberger/Z3.jl)はZ3のC APIをラップしています。以前のバージョンはC++ APIをラップしていました。Juliaバインディングの更新とビルドに関する情報は[src/api/julia](https://github.com/z3prover/z3/blob/master/src/api/julia)にあります。 ### ``WebAssembly`` / ``TypeScript`` / ``JavaScript`` 関連するTypeScript型定義を伴うWebAssemblyビルドは、[z3-solver](https://www.npmjs.com/package/z3-solver)としてnpmで公開されています。これらのバインディングのビルドに関する情報は[src/api/js](https://github.com/z3prover/z3/blob/master/src/api/js)にあります。 ### Smalltalk (``Pharo`` / ``Smalltalk/X``) プロジェクト[MachineArithmetic](https://github.com/shingarov/MachineArithmetic)は、Z3のC APIへのSmalltalkインターフェースを提供します。詳細については、[MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md)を参照してください。 ### AIX [AIX向けのビルド設定はこちらで説明されています。](https://github.com/Z3Prover/z3/pull/8113) ## システム概要  ## インターフェース * デフォルトの入力形式は[SMTLIB2](http://smtlib.cs.uiowa.edu)です * その他のネイティブ外部関数インターフェース: * [C++ API](https://z3prover.github.io/api/html/namespacez3.html) * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) * [Python API](https://z3prover.github.io/api/html/namespacez3py.html)（[pydoc形式](https://z3prover.github.io/api/html/z3.html)でも利用可能） * [Rust](https://github.com/prove-rs/z3.rs) * C * OCaml * [Julia](https://github.com/ahumenberger/Z3.jl) * [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md)（PharoとSmalltalk/Xをサポート） ## パワーツール * 現在ETH Zurichによって開発されている[Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) # ファズバグ報告に関するポリシー Z3はファザーにとって人気のターゲットです。z3やSMTソルバのバグ発見に関する（優れた）論文が数多く発表されており、ファズツールの価値に関する出版物の証拠を確立する上で、バグ報告数と修正数の比率が重要な役割を果たしていることは間違いありません。 残念ながら、ファズバグへの対応は、ユーザーにとって最も重要な場面でのz3の利用を必ずしも前進させるものではなく、それらへの対応に費やす労力はそうした活動から時間を奪います。 診断と修正のためのコーディングエージェントの品質が急速に向上している現在、ファズバグ報告に対して診断と修正にしっかりと取り組むことを求めるのは合理的な要請です。 取り組みを重要なことに集中させるため、再現手順以上の分析を含まないファズバグは、それ以上の検討なしにクローズされる場合があります。
