The Z3 Theorem Prover
3 months ago
- #Microsoft-Research
- #programming-languages
- #theorem-prover
- Z3是微软研究院开发的定理证明器，采用MIT许可证授权。
- 提供稳定版和每日构建版的预编译二进制文件下载。
- 支持通过Visual Studio、Makefile、CMake、vcpkg或Bazel构建Z3。
- 提供多种编程语言接口支持，包括C++、Java、.NET、OCaml和Python。
- MSVC版本默认启用控制流防护(Control Flow Guard)和地址空间布局随机化(ASLR)等安全特性。
- 构建Z3需要Python环境，可选安装GMP库以支持多精度整数运算。
- Z3默认采用SMTLIB2输入格式，并支持多种外部函数接口。
- WebAssembly版本可通过npm包z3-solver获取。
- Julia语言的Z3.jl包封装了Z3的C语言接口。