python - z3py 示例不适用于 macOS

Question

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

我已经包含了一个例子来说明。

代码:

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

Error: Traceback (most recent call last): File "test.py", line 3, in x = Int('x') NameError: name 'Int' is not defined

如果有任何帮助，我将不胜感激。非常感谢。

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 机器或构建过程。