用户可借助该项目进行定理证明相关工作。它提供多语言绑定，支持C++、.NET、Java、Python等，具备多种构建方式，依赖少且功能强大。【此简介由AI生成】
Z3
Z3 是微软研究院开发的一款定理证明器。
它基于 MIT 许可证 授权使用。
如果您还不熟悉 Z3，可以从这里开始了解。
稳定版和每日构建的预编译二进制文件可从此链接获取。
Z3 可通过 Visual Studio、Makefile 或 CMake 进行构建，并支持多种编程语言的绑定。
各稳定版本的更新说明请参阅发布日志。
构建状态
| Azure Pipelines |
|---|
 |
在 Windows 上使用 Visual Studio 命令提示符构建 Z3
32 位构建，请以以下命令开始：
python scripts/mk_make.py
或者，对于 64 位版本：
python scripts/mk_make.py -x
随后：
cd build
nmake
Z3 采用 C++17 标准开发，因此推荐使用 Visual Studio 2019 版本。
使用 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 绑定外，推荐将其用于大多数构建任务。
依赖项
Z3 本身依赖项较少，仅需 C++ 运行时库（包括用于多线程的 pthreads）。用户可选择使用 GMP 处理多精度整数运算，但 Z3 已内置完整的多精度运算功能。构建 Z3 需安装 Python。构建 Java、.NET、OCaml 和 Julia 接口需安装相应工具链。
Z3 语言绑定
Z3 支持多种编程语言接口。
.NET
可从 nuget.org 安装最新版 Z3 的 NuGet 包。
使用 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
可通过以下命令从 PyPI 安装最新版 Z3 的 Python 封装：
pip install z3-solver
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 中的示例。
Julia
Julia 包 Z3.jl 封装了 Z3 的 C++ API。有关更新和构建 Julia 绑定的信息可在 src/api/julia 中找到。
Web Assembly
WebAssembly 绑定由 Clément Pit-Claudel 提供。
系统概览
