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 文档和教程似乎没有提到这个或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