python - Z3 Python 绑定：在使用 Z3-python 之前必须调用 init(Z3_LIBRARY_PATH)

Question

我在 Linux 上安装了Z3 定理证明器，并且正在使用它的 Python 绑定 (Z3Py)。我试图测试一个最小的例子，但我立即收到以下错误：

z3.z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python

如何解决此问题并启动并运行 Z3？

我不太确定该错误消息的含义。Z3 文档和教程似乎没有提及 this 或 about init()，Z3-Python 文档也没有列出任何名为init().

更详细地说，这是我尝试过的（略摘录）：

$ python
Python 2.7.13 (default, Jan 12 2017, 17:59:37)
>>> from z3 import *
>>> Int('x')
Traceback (most recent call last):
  ...
  File "/usr/lib64/python2.7/site-packages/z3/z3core.py", line 22, in lib
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3.z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python

我尝试在运行 Python 之前设置一个名为的环境变量Z3_LIBRARY_PATH，这可能会有所帮助，但这没有任何区别。

Answer 1

导入 Z3 库后，调用

init('/usr/lib64/python2.7/site-packages/z3')

在调用任何其他 Z3 API 之前。您可能需要调整路径：将其更改libz3.so为找到的路径。（试着locate libz3.so找到它，如果它不在一个明显的地方。）

示例用法：

$ python
Python 2.7.13 (default, Jan 12 2017, 17:59:37)
>>> from z3 import *
>>> init('/usr/lib64/python2.7/site-packages/z3')
>>> Int('x')
x