z3下載 - z3原始碼下載

z3

其他源碼

z3-4.13.3

下載

Z3

Z3是微軟研究院的定理證明器。它是根據 MIT 許可證獲得許可的。

如果您不熟悉Z3，可以從這裡開始。

可從此處取得用於穩定版本和夜間版本的預先建置二進位檔案。

Z3 可以使用 Visual Studio、Makefile 或使用 CMake 來建置。它提供了多種程式語言的綁定。

有關 Z3 各種穩定版本的說明，請參閱發行說明。

Docker 映像。

使用 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。

使用 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 位元建置也是如此。

預設情況下，它將在PREFIX/bin安裝 z3 可執行文件，在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 輕鬆安裝 libzmq。

執行：

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

依賴關係

Z3 本身幾乎沒有依賴性。它使用 C++ 運行時庫，包括用於多線程的 pthreads。可以選擇將 GMP 用於多精度整數，但 Z3 包含其自己的獨立多精度功能。建置 Z3 需要 Python。要建置Java、.Net、OCaml、Julia API，需要安裝相關工具鏈。

Z3 綁定

Z3 具有多種程式語言的綁定。

`.NET`

您可以從 nuget.org 安裝最新版本 Z3 的 nuget 套件。

將--dotnet命令列標誌與mk_make.py一起使用來啟用建置這些。

有關範例，請參閱examples/dotnet 。

`C`

這些始終處於啟用狀態。

有關範例，請參見examples/c 。

`C++`

這些始終處於啟用狀態。

有關範例，請參閱examples/c++ 。

`Java`

將--java命令列標誌與mk_make.py一起使用來啟用建置它們。

有關範例，請參閱examples/java 。

`OCaml`

將--ml命令列標誌與mk_make.py一起使用來啟用建置它們。

有關範例，請參閱examples/ml 。

`Python`

您可以使用以下命令從 pypi 安裝最新版本的 Z3 的 Python 包裝器：

   pip install z3-solver

將--python命令列標誌與mk_make.py一起使用來啟用建置它們。

請注意，在某些平台上，Python 套件目錄（大多數發行版上的site-packages和基於 Debian 的發行版上的dist-packages ）需要位於 install 前綴下。如果您使用非標準前綴，則可以使用--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 。