python - 本地使用 Z3Py

Question

我通过 IDLE GUI 在 Windows XP 上使用 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。