python中的Z3代码

Question

我已经安装了 python 和 Z3 并设置了 PYTHONPATH 与 Z3 python 目录的路径。

我通过运行 from z3 import * 导入 Z3

但在此之后，我收到一条持续的长错误消息，其以以下方式结束：

File "C:\Program Files\Microsoft Research\Z3-4.1\python\z3core.py", line 34, in init
    _lib = ctypes.CDLL(PATH)
  File "C:\Python27\lib\ctypes\__init__.py", line 365, in __init__
    self._handle = _dlopen(self._name, mode)
WindowsError: [Error 126] The specified module could not be found

有趣的是，一切都正常，直到我重新安装了 python 和 Z3。

Answer 1

您的 PATH 环境变量应设置为包含 Z3 安装中的 bin 或 x64 目录。如果您使用 64 位版本的 Python，则应包含 x64 目录。

例子：

hello.py .... 文件“C:\Python27\lib\ctypes__init__.py”，第 365 行，在init self._handle = _dlopen(self._name, mode) WindowsError: [Error 126] 指定的模块无法成立

设置 PATH=%PATH%;C:\Program Files (x86)\Microsoft Research\Z3-4.1\bin

hello.py 回溯（最近一次调用最后一次）：.... 文件“C:\Python27\lib\ctypes__init__.py”，第 365 行，init self._handle = _dlopen(self._name, mode) WindowsError: [Error 193] %1 不是有效的 Win32 应用程序

设置 PATH=%PATH%;C:\Program Files (x86)\Microsoft Research\Z3-4.1\x64

你好.py 你好 Z3