在 Eclipse (pydev) 上安装 z3

【问题标题】：Installing z3 on eclipse (pydev)在 Eclipse (pydev) 上安装 z3
【发布时间】：2016-06-06 19:27:33
【问题描述】：

无法让 z3 在 pydev 上运行。

下载z3后，我去eclipse windows > Preferences > PyDev > Interpreters > Python Interpreters 然后将“z3/bin”添加到库中

运行 Python 2.7.11 和 z3 32 位

当我尝试运行简单代码时

from z3 import*  

x = Int('x')
y = Int('y')

print simplify(x + y + 2*x + 3)

得到错误

NameError: name 'Int' is not defined

【问题讨论】：

【解决方案1】：

尝试按照 PyDev 手册中的说明将 z3 添加到 forced builtins：

（即：可能该信息是动态给出的，这意味着您必须让 PyDev 使用 shell 动态计算给您 - 否则，默认情况下 PyDev 只会尝试静态分析代码）。

【讨论】：

所以如果我按照正确的操作我做到了：Windows > Preferences > PyDev > Interpreters > Python Interpreters > Forced Builtins Tab > New > typed z3 > apply > ok。如果还是一样的错误。
在深入了解 PyDev 中可能出现的问题之前：该脚本是否在命令行中工作？
你能比较一下命令行中的pythonpath和PyDev中的pythonpath吗？即：在该脚本的开头运行：import sys;print('\n'.join(sorted(sys.path))) 看看是否有什么不同。
你能做到：import z3;print(z3) 在每种情况下，看看它是否真的在导入相同的模块？（即：您可能正在隐藏该导入）
在 Eclipse 上我得到：NameError: name 'z3' is not defined。在控制台上我得到：跨度>