z3
z3-4.13.3
Z3 は Microsoft Research の定理証明者です。 MITライセンスに基づいてライセンスされています。
Z3 に慣れていない場合は、ここから始めてください。
安定版および夜間リリース用の事前構築済みバイナリは、ここから入手できます。
Z3 は、Visual Studio、Makefile、または CMake を使用してビルドできます。いくつかのプログラミング言語のバインディングを提供します。
Z3 のさまざまな安定リリースに関する注意事項については、リリース ノートを参照してください。
ドッカーイメージ。
32 ビット ビルドは次から始めます。
python scripts/mk_make.pyまたは、64 ビット ビルドの場合は次のようにします。
python scripts/mk_make.py -xそれから：
cd build
nmakeZ3 は C++20 を使用します。したがって、Visual Studio の推奨バージョンは VS2019 です。
実行する：
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.pyClang < 3.7 は OpenMP をサポートしていないことに注意してください。
Cygwin と Mingw-w64 クロスコンパイラーを使用して Windows 用の Z3 をビルドすることもできます。このケースを正しく設定するには、Windows にインストールされた Python ではなく、Cygwin 独自の 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.py32 ビット ビルドも同様に動作するはずです (ただし、テストはされていません)。 Cygwin32 内からの 32/64 ビット ビルドにも同じことが当てはまります。
デフォルトでは、z3 実行可能ファイルはPREFIX/binに、ライブラリmk_make.py PREFIX/libに、インクルード ファイルはPREFIX/includeにインストールされます。PREFIX インストール プレフィックスはPREFIXスクリプトによって推測されます。通常、ほとんどの Linux ディストリビューションの場合は/usr 、FreeBSD および macOS の場合は/usr/localです。 --prefix=コマンド ライン オプションを使用して、インストール プレフィックスを変更します。例えば：
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make installZ3 をアンインストールするには、次を使用します。
sudo make uninstall Z3 をクリーンアップするには、ビルド ディレクトリを削除し、 mk_make.pyスクリプトを再度実行します。
Z3 には CMake を使用したビルド システムがあります。詳細については、README-CMake.md ファイルをお読みください。 OCaml バインディングのビルドを除く、ほとんどのビルド タスクに推奨されます。
vcpkg は完全なプラットフォームのパッケージ マネージャーであり、vcpkg を使用して libzmq を簡単にインストールできます。
実行する：
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3Z3 自体には依存関係がほとんどありません。マルチスレッド用の pthread を含む C++ ランタイム ライブラリを使用します。オプションで多精度整数に GMP を使用することも可能ですが、Z3 には独自の自己完結型多精度機能が含まれています。 Z3 をビルドするには Python が必要です。 Java、.Net、OCaml、Julia API を構築するには、関連するツール チェーンをインストールする必要があります。
Z3 にはさまざまなプログラミング言語用のバインディングがあります。
.NET最新リリース Z3 の nuget パッケージを nuget.org からインストールできます。
これらのビルドを有効にするには、 mk_make.pyで--dotnetコマンド ライン フラグを使用します。
例については、 examples/dotnet参照してください。
Cこれらは常に有効になっています。
例については、 examples/c参照してください。
C++これらは常に有効になっています。
例については、 examples/c++参照してください。
Javaこれらのビルドを有効にするには、 mk_make.pyで--javaコマンド ライン フラグを使用します。
例については、 examples/java参照してください。
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
# 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参照してください。
JuliaJulia パッケージ Z3.jl は、Z3 の C API をラップします。以前のバージョンでは C++ API がラップされていました。Julia バインディングの更新と構築に関する情報は、src/api/julia にあります。
Web Assembly / TypeScript / JavaScript関連する TypeScript タイピングを含む WebAssembly ビルドは、npm で z3-solver として公開されます。これらのバインディングの構築に関する情報は、src/api/js にあります。
Pharo / Smalltalk/X )Project MachineArithmetic は、Z3 の C API に Smalltalk インターフェイスを提供します。詳細については、MachineArithmetic/README.md を参照してください。
デフォルトの入力形式は SMTLIB2 です
その他のネイティブ外部関数インターフェイス:
C++ API
.NET API
Java API
Python API (pydoc 形式でも利用可能)
さび
C
OCaml
ジュリア
Smalltalk (Pharo および Smalltalk/X をサポート)
