我已经使用Anaconda Prompt(pip-install z3 solver(在我的Python3环境中安装了PyPi的z3 solver包，仅此而已。
该软件包出现在站点软件包/目录中(该软件包具有_init__.py和包括z3.py在内的所有重要文件(。然而，当我尝试从Jupyter Notebook运行此示例时，它返回以下消息：NameError：名称"Int"未定义。
我只使用蟒蛇很短的时间，所以我不确定安装是如何工作的。这真的很奇怪，因为"pip-install"命令在大多数情况下都能正常工作。是我做错了什么，还是这个包需要更多的配置？
您必须编写：
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)
您可以运行conda install pip，然后运行pip install z3-solver。
很抱歉更新延迟。
我根据这本指南设法解决了这个问题。
为了永久更改Anaconda,中的sys.path变量，我创建了一个包含z3路径的.PTH file，并将其放在站点包目录中。
您可能需要将libz3.dll文件复制到正确的目录才能使其工作。运行pip install z3-solver确实下载了所需的文件，并将它们放入站点包中，但我无法从任何地方导入z3。
也许你还需要在使用pip后修复路径，以便蟒蛇能够识别它。我手动完成了所有操作，所以我不确定为什么pip在这种情况下不起作用。
这就是我在Windows上安装z3所做的全部工作。希望它能有所帮助！
在2022年也遇到了同样的问题。
重要信息：
使用以下命令安装
pip install z3 z3-solver
我不知道z3求解器包，所以我后来安装了它，但它不起作用。和你一样的问题。可以导入，但导入只包含六个特殊的dunder函数，如__file__和其他函数。
在安装、卸载、添加到-$PATH的所有步骤之后。。。后来我就这么做了，而且马上就奏效了。
很多答案，但我遇到了这个问题，发现：
- 首先，
pip install z3安装了一个与AWS备份相关的过时且不相关的包 - 其次，
pip install z3-solver只安装到z3系统的已安装安装的接口，python库名称为z3。它不安装底层z3系统，并且警告您它不存在。如果没有底层系统；从z3导入*"；将执行，但不会导入任何有用的函数 - 第三，安装z3最简单的方法是使用您喜欢的软件包管理器。在macOS上，我使用了
brew install z3
当两个部件的安装都工作时，一个好的快速测试是import * from z3; a,b = Reals('a b')。如果这些语句得到执行，你就很好。