z3
z3-4.13.3
Z3是微软研究院的定理证明器。它是根据 MIT 许可证获得许可的。
如果您不熟悉Z3，可以从这里开始。
可从此处获取用于稳定版本和夜间版本的预构建二进制文件。
Z3 可以使用 Visual Studio、Makefile 或使用 CMake 来构建。它提供了多种编程语言的绑定。
有关 Z3 各种稳定版本的说明，请参阅发行说明。
Docker 镜像。
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.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.py32 位构建应该类似地工作（但未经测试）；对于 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脚本。
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 本身几乎没有依赖性。它使用 C++ 运行时库，包括用于多线程的 pthreads。可以选择将 GMP 用于多精度整数，但 Z3 包含其自己的独立多精度功能。构建 Z3 需要 Python。要构建Java、.Net、OCaml、Julia API，需要安装相关工具链。
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 。
JuliaJulia 包 Z3.jl 包装了 Z3 的 C API。它的早期版本包装了 C++ API：有关更新和构建 Julia 绑定的信息可以在 src/api/julia 中找到。
Web Assembly / TypeScript / JavaScript具有关联 TypeScript 类型的 WebAssembly 构建作为 z3-solver 在 npm 上发布。有关构建这些绑定的信息可以在 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
奥卡米尔
朱莉娅
Smalltalk（支持 Pharo 和 Smalltalk/X）
