z3py 示例不适用于 macOS

Question

我无法让任何 z3py 示例运行。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了 python 路径以指向适当的目录。此外，我能够成功导入 z3，但每次声明变量时都会出现错误。编译器无法识别 Int、Ints、Real 、 RealVal。

我举了一个例子来说明。

代码：

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

错误： 回溯（最近一次调用最后一次）： 文件“test.py”，第 3 行，位于 x = Int('x') NameError：名称“Int”未定义

我真的很感激任何帮助。非常感谢。

Answer 1

您的本地安装有问题，无论是 Python 还是 Z3。

我刚刚在我的 Mac 上编译了 Z3 并运行了您提供的示例

test.py

，没有任何问题。我使用 OS X 10.9.5 和 Python 2.7.11 以及 Z3 的当前主版本（提交 41edf5f）。我使用的确切说明是：

git clone https://github.com/Z3Prover/z3.git
cd z3
./configure
cd build
make -j4
emacs test.py
# Write in the example you gave.
python ./test.py

我得到的输出是

[y = 0, x = 7]

，这与我从 Linux 机器上的脚本中得到的输出相同。因此，该问题特定于您的 OS X 机器或构建过程。

Answer 2

尝试安装

z3-solver

：

pip install z3-solver

与

z3

存在名称冲突