问安装了Z3解决程序，但我不能导入任何东西

EN

你必须写：

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。

抱歉更新得太晚了。

我已经设法解决了基于本指南的问题。

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

您可能需要将libz3.dll文件复制到正确的目录中，这样它才能工作。运行pip install z3-solver确实会下载所需的文件并将它们放在站点包中，但是我不能从任何地方导入z3。

也许你也需要在使用pip后修复路径，这样Anaconda就可以识别它了。我手动做了所有的事情，所以我不知道为什么pip在这种情况下不起作用。

这就是我在我的Windows上安装Windows所做的全部工作。希望能帮上忙！