0

我正在尝试在 Eclipse IDE中使用 Z3 ( http://z3.codeplex.com/ )。我安装了 PyDev 并下载了 Z3 的预编译 Windows 二进制文件。我还将“bin”子目录添加到环境变量 PYTHONPATH 和 PATH 中。

在这个非常简单的例子中，

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()

Eclipse 说 Real e Solver 是未定义的变量。运行此代码我收到此错误消息：

“ImportError: Bad magic number in ...\bin\z3.pyc”

似乎这是与解释器不同的python版本（通常较晚）的问题（请参阅：What's the bad magic number error？）。

有什么帮助吗？我是否需要编译和安装 Z3Py 而不是使用预编译的 Windows 二进制文件？

谢谢。

4

1 回答 1

0

我对在 Eclipse 中使用 Python 不是很熟悉，但这很可能确实是因为 Python 版本不匹配。最安全的方法可能是安装 32 位版本的 Python 2.7.x 并确保 Eclipse 也使用该版本。或者，您可以自己编译 Z3，使用您最喜欢的 Python 版本进行 Python 绑定。我建议使用不稳定的分支，因为它包含许多尚未集成到主分支中的修复（有关编译说明，请参阅README）。请注意，在 Codeplex 的“计划”部分中也有用于不稳定分支的预编译 Windows 二进制文件（请参阅此处），这可能会解决此问题。

于 2014-01-16T16:33:28.730 回答