Z3Prover/z3

# Z3 Z3 是来自 Microsoft Research 的定理证明器。 它基于 [MIT 许可证](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 可以使用 [Visual Studio][1]、[Makefile][2]、[CMake][3]、[vcpkg][4] 或 [Bazel][5] 进行构建。 它提供了[多种编程语言的绑定][6]。 有关 Z3 各个稳定版本的说明，请参阅[发行说明](RELEASE_NOTES.md)。 [](https://microsoft.github.io/z3guide/) ## 构建状态 ### Pull Request & Push 工作流 | WASM 构建 | Windows 构建 | CI | OCaml 绑定 | | ------------|---------------|----|-----------| | [](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/ocaml.yaml) | ### 计划工作流 | Open Bugs | Android 构建 | Pyodide 构建 | 每日构建 | 交叉构建 | | -----------|---------------|---------------|---------------|-------------| | [](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nightly.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/cross-build.yml) | | MSVC Static | MSVC Clang-CL | 构建 Z3 缓存 | 代码覆盖率 | 内存安全 | 标记 PR 准备就绪 | |-------------|---------------|----------------|---------------|---------------|----------------| | [](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/coverage.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/mark-prs-ready-for-review.yml) | ### 手动与发布工作流 | 文档 | 发布构建 | WASM 发布 | NuGet 构建 | |---------------|---------------|--------------|-------------| | [](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/nuget-build.yml) | ### 专用工作流 | 每日验证 | Copilot 设置 | Agentics 维护 | |--------------------|---------------|----------------------| | [](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) | ### 智能体工作流 | A3 Python | API 一致性 | 代码简化器 | 发行说明 | 工作流建议 | | ----------|---------------|-----------------|---------------|---------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/a3-python.lock.yml) | [](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) | | 学术引用 | 构建警告修复器 | 代码规范 | CSA 报告 | 待办问题 | | ------------------|---------------------|------------------|------------|---------------| | [](https://github.com/Z3Prover/z3/actions/workflows/academic-citation-tracker.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/build-warning-fixer.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-conventions-analyzer.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/csa-analysis.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/issue-backlog-processor.lock.yml) | | 内存安全报告 | Ostrich 基准测试 | QF-S 基准测试 | Tactic-to-Simplifier | ZIPT 代码审查 | | ---------------------|-------------------|----------------|----------------------|--------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety-report.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ostrich-benchmark.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/qf-s-benchmark.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/tactic-to-simplifier.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/zipt-code-reviewer.lock.yml) | ## 在 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 默认启用了几项安全特性： - Control Flow Guard (`/guard:cf`) - 默认启用，通过阻止对函数入口点以外位置的调用来检测破坏代码的尝试，使攻击者更难通过控制流重定向执行任意代码 - 地址空间布局随机化 (`/DYNAMICBASE`) - 默认启用用于内存布局随机化，这是 `/GUARD:CF` 链接器选项所必需的 - 如有需要，可以使用 `python scripts/mk_make.py --no-guardcf`（Python 构建）或 `cmake -DZ3_ENABLE_CFG=OFF`（CMake 构建）禁用这些特性 ## 使用 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](README-CMake.md) 文件。除了构建 OCaml 绑定之外，它推荐用于大多数构建任务。 ## 使用 vcpkg 构建 Z3 vcpkg 是一个全平台包管理器。要使用 vcpkg 安装 Z3，请执行： ``` 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 本身只有很少的依赖项。它使用 C++ 运行时库，包括用于多线程的 pthreads。 可选地，可以使用 GMP 进行多精度整数运算，但 Z3 包含其自包含的 多精度功能。构建 Z3 需要 Python。构建 Java、.NET、OCaml 和 Julia API 需要安装相关的工具链。 ## Z3 绑定 Z3 为多种编程语言提供了绑定。 ### ``.NET`` 您可以从 [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/) 安装最新版本 Z3 的 NuGet 包。 在 ``mk_make.py`` 中使用 ``--dotnet`` 命令行标志以启用这些构建。 有关示例，请参见 [``examples/dotnet``](examples/dotnet)。 ### ``C`` 这些总是启用的。 有关示例，请参见 [``examples/c``](examples/c)。 ### ``C++`` 这些总是启用的。 有关示例，请参见 [``examples/c++``](examples/c++)。 ### ``Java`` 在 ``mk_make.py`` 中使用 ``--java`` 命令行标志以启用这些构建。 有关 IDE 设置说明（Eclipse、IntelliJ IDEA、Visual Studio Code）和故障排除，请参阅 [Java IDE 设置指南](doc/JAVA_IDE_SETUP.md)。 有关示例，请参见 [``examples/java``](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``](src/api/go/README.md)。 ### ``OCaml`` 在 ``mk_make.py`` 中使用 ``--ml`` 命令行标志以启用这些构建。 有关示例，请参见 [``examples/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 虚拟环境](https://virtualenv.readthedocs.org/en/latest/) 并在那里安装 Z3。Python 包也适用于 Python3。 在 Windows 下，请记住在 Visual C++ 本机命令构建环境中进行构建。 请注意，从使用 Python 运行 Z3 的位置应该能够访问 ``build/python/z3`` 目录， 并且它要求 ``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``](examples/python)。 ### ``Julia`` Julia 包 [Z3.jl](https://github.com/ahumenberger/Z3.jl) 封装了 Z3 的 C API。它的先前版本封装的是 C++ API：有关更新和构建 Julia 绑定的信息，可以在 [src/api/julia](src/api/julia) 中找到。 ### ``WebAssembly`` / ``TypeScript`` / ``JavaScript`` 带有相关 TypeScript 类型定义的 WebAssembly 构建已作为 [z3-solver](https://www.npmjs.com/package/z3-solver) 发布在 npm 上。有关构建这些绑定的信息，可以在 [src/api/js](src/api/js) 中找到。 ### Smalltalk（``Pharo`` / ``Smalltalk/X``） 项目 [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) 提供了 Smalltalk 接口连接到 Z3 的 C API。有关更多信息，请参阅 [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） ## 强大工具 * [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) 目前由 ETH Zurich 开发

标签：AI工具, Bash脚本, Bazel, C++, CMake, JS文件枚举, Makefile, OCaml, Python, SAT求解, SMT求解器, TLS抓取, vcpkg, Visual Studio, WASM, Z3, 可配置连接, 多人体追踪, 定理证明器, 开源, 形式化验证, 微软研究院, 数学逻辑, 数据擦除, 无后门, 日志审计, 漏洞分析, 漏洞数据库, 程序分析, 符号执行, 约束求解, 自动定理证明, 路径探测, 软件安全, 逆向工具