在本地使用 Z3Py

Question

我在 Windows XP 上通过 IDLE GUI 使用 Python 2.7.3，并尝试通过 Python API 在本地运行 Z3 4.0。

这条线工作正常：

>>> from z3 import *

这行没有：

>>> x = Int('x')

Traceback (most recent call last):
[...]
  File "C:\Program Files\Microsoft Research\Z3-4.0\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

有人知道问题出在哪里吗？

我的 PYTHONPATH 设置为“C:\Program Files\Microsoft Research\Z3-4.0\python”，不带引号。

Answer 1

Z3 使用线程本地存储。它是使用 __declspec(thread) 实现的。不幸的是，Windows XP 和 Server 2003 中的 DLL 不支持此功能。来自 MSN 文档：

“对于在进程启动后动态加载的 DLL（延迟加载、COM 对象、显式 LoadLibrary 等），__declspec(thread) 在 Windows XP、2003 Server 和更早的操作系统上不起作用，但在 Vista 和2008 服务器。”

因此，要使用 Z3 DLL，您必须使用以下 Windows 之一：8、7、Vista 或 Server 2008。

Answer 2

在 Windows XP 上，文件名中的空格可能会导致 python 无法找到 z3.dll；这似乎是一个一般的 python 问题，请参阅，例如： some notes on PYTHONPATH

如果使用旧的 8.3 格式的目录，它可能会起作用。您可以通过在命令外壳中找到 Z3 目录来找到短名称（我使用 dir /x 在 Windows 7 上查看短名称），在我的系统上，短路径是 C:\progra~1\mi4430~1\z3 -4.0\bin。不过，这些数字在每次安装时都不同。

一个更快的解决方案可能是简单地将 z3.dll 从 bin 目录复制到 python 目录（或者如果您使用 64 位，则从 x64 目录复制）。