section.0 介绍

Z3是微软研究院的定理证明器。它是根据MIT 许可证获得许可的。

如果您不熟悉Z3，可以从这里开始。

z3实例

section.1 关于安装

1
pip install z3-solver

使用上面命令即可，但是有可能会出现下图这种bug

image-20241026153556116

若出现此类情况，建议查看已经安装的软件包

如果存在z3这个老软件包，先卸载：

1
2
pip uninstall z3
pip uninstall z3-solver

然后重新安装即可

section.2 应用