已安装 Z3 求解器，但我无法导入任何内容答案

【问题标题】：Z3 solver installed but I can't import anything已安装 Z3 求解器，但我无法导入任何内容
【发布时间】：2020-04-12 11:51:39
【问题描述】：

我已经使用 Anaconda Prompt ( pip install z3-solver ) 在我的 Python3 环境中从 PyPi 安装了 z3-solver 包，仅此而已。
包出现在site-packages/ 目录中（包有 _init__.py 和所有必要的文件，包括 z3.py ）。但是，当我尝试从 Jupyter Notebook 运行 this example 时，它返回以下消息：NameError: name 'Int' is not defined。
我只使用了很短的时间 Anaconda，所以我不确定安装是如何工作的。这真的很奇怪，因为“pip install”命令在大多数情况下都能正常工作。我做错了什么还是这个包需要更多配置？

【问题讨论】：

将 Int 更改为 int
它不起作用。 Int 是在 z3 中定义的一个类，我使用的示例取自他们的官方 Github repo，因此它与语法无关。
你的项目目录中有一个名为z3.py的文件吗？
您是否遵循了在 Conda 中使用 pip 的建议？参见，例如：anaconda.com/using-pip-in-a-conda-environment。

标签： python anaconda conda z3

【解决方案1】：

你必须写：

from z3 import *

解决了我的NameError: name 'Solver' is not defined 异常

先决条件：

pip install z3
pip install z3-solver

代码示例

from z3 import *
 
def main(): 
    
    s = Solver()
    x = Int('x')
    y = Int('y')
    s.add(x < 10)

【讨论】：

【解决方案2】：

抱歉更新晚了。

我已经根据this guide解决了这个问题。

为了永久更改Anaconda, 中的sys.path 变量，我创建了一个.PTH file，其中包含z3 的路径并将其放在site-packages 目录中。

您可能需要将libz3.dll 文件复制到正确的目录才能使其正常工作。运行 pip install z3-solver 确实会下载所需的文件并将它们放入 site-packages 但我无法从任何地方导入 z3。

也许您还需要在使用 pip 后修复路径，以便 Anaconda 可以识别它。我手动完成了所有操作，所以我不确定为什么 pip 在这种情况下不起作用。

这就是我在Windows 上安装z3 所做的一切。希望能帮助到你！

【讨论】：

【解决方案3】：

您可以运行conda install pip，然后运行pip install z3-solver。

【讨论】：