python - python 中的 Z3 代码

Question

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

我通过运行它来导入 Z3，从 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 .... 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

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

hello.py Traceback (most recent call last): .... File "C:\Python27\lib\ctypes__init__.py", line 365, in init self._handle = _dlopen(self._name, mode) WindowsError: [Error 193] %1 is not a valid Win32 application

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

hello.py hello Z3