Python导入z3模块后无法调用Solver函数，报NameError问题求助

哎，这个问题我之前也碰到过好几次，大概率是以下几个常见坑之一，咱们一步步排查：

• 脚本文件名和Z3模块重名了
  这是最容易踩的坑！如果你把自己的Python脚本命名成了z3.py，那Python在执行from z3 import *的时候，会优先导入你自己写的这个脚本，而不是真正的Z3库。你的脚本里当然没有Solver类，所以调用就会报NameError。
  解决办法很简单：把你的脚本改成别的名字（比如z3_demo.py），然后删除当前目录下的z3.pyc文件和__pycache__文件夹（如果有的话），避免缓存干扰。

• Python环境和Z3安装环境不匹配
  如果你电脑上装了多个Python版本（比如Python3.7和Python3.10），可能会出现pip把Z3装到了其中一个版本，但你运行脚本用的是另一个版本的Python。这种情况下，导入的其实不是安装了Z3的环境里的模块，自然找不到Solver。
  你可以先在终端运行这条命令验证：

  python -c "import z3; print(z3.__file__)"
  

  看看输出的路径是不是你预期的Z3安装位置。如果不对，就用对应版本的pip重新安装（比如pip3 install z3-solver），或者直接用对应版本的Python运行脚本（比如python3.10 your_script.py）。

• 代码里不小心覆盖了Solver名称
  检查一下你的代码，有没有在from z3 import *之后，定义了一个叫Solver的变量或者函数？比如：

  from z3 import *
  Solver = "some string"  # 这里覆盖了Z3的Solver类
  s = Solver()  # 自然会报错！
  

  如果有这种情况，把变量名改成别的（比如my_solver_name）就行。

快速测试方法 #

你可以先写一个极简的测试脚本，排除代码本身的问题：

from z3 import *
s = Solver()
x = Int('x')
s.add(x > 5)
print(s.check())
print(s.model())

如果这个脚本能正常运行，输出sat和[x = 6]之类的结果，那问题肯定出在你原来的代码里；如果还是报错，那就是前面两种环境或文件名的问题。

内容的提问来源于stack exchange，提问作者DocGurk