Z3

Z3 是微软研究院开发的一款定理证明器。它采用 MIT 许可证进行授权。Windows 二进制发行版包含 C++ 运行时可再分发组件。

如果你不熟悉 Z3，可以从这里开始了解。

稳定版和 nightly 版本的预编译二进制文件可在此处获取。

Z3 可以使用 Visual Studio、Makefile、CMake、vcpkg 或 Bazel 构建。它还为多种编程语言提供了绑定。

有关 Z3 各个稳定版本的说明，请参阅发布说明。

构建状态

Pull Request 和 Push 工作流

WASM 构建	Windows 构建	CI	OCaml 绑定

计划性工作流

开放缺陷	Android 构建	Pyodide Wheel (PyPI)	Nightly 构建	交叉构建

MSVC 静态	MSVC Clang-CL	构建 Z3 缓存	内存安全	标记 PR 就绪

手动和发布工作流

文档	发布构建	WASM 发布	NuGet 构建

专门工作流

Nightly 验证	Copilot 设置	Agentics 维护

智能体工作流

API 一致性	代码简化器	发布说明	工作流建议	学术引用

问题积压	内存安全报告	QF-S 基准测试	Specbot 崩溃分析器	SMTLIB 基准查找器

TPTP 基准测试

在 Windows 上使用 Visual Studio 命令提示符构建 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 构建中禁用这些特性，可使用 python scripts/mk_make.py --no-guardcf；在 CMake 构建中，可使用 cmake -DZ3_ENABLE_CFG=OFF

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

你可以从 nuget.org 为最新发布的 Z3 安装 NuGet 包。

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

你可以使用以下命令从 pypi 安装最新发布的 Z3 Python 包装器：

   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 构建已作为 z3-solver 发布到 npm。有关构建这些绑定的信息，请参见 src/api/js。

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

项目 MachineArithmetic 提供了 Z3 C API 的 Smalltalk 接口。更多信息，请参见 MachineArithmetic/README.md。

AIX

此处描述了 AIX 上的构建设置。

系统概述

系统图

接口

默认输入格式为 SMTLIB2
其他原生外部函数接口：
C++ API
.NET API
Java API
Python API（也可在 pydoc 格式中找到）
Rust
C
OCaml
Julia
Smalltalk（支持 Pharo 和 Smalltalk/X）

强力工具

由苏黎世联邦理工学院 (ETH Zurich) 当前开发的 Axiom Profiler

z3 z3-5.0.0

分类