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

【问题标题】：Z3 Python bindings: init(Z3_LIBRARY_PATH) must be invoked before using Z3-pythonZ3 Python 绑定：在使用 Z3-python 之前必须调用 init(Z3_LIBRARY_PATH)
【发布时间】：2017-08-20 16:30:16
【问题描述】：

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

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

如何解决这个问题并开始使用 Z3？

我不太确定该错误消息的含义。 Z3 文档和教程似乎没有提到这个或 init()，Z3-Python docs 没有列出任何名为 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 的环境变量，这可能会有所帮助，但没有任何区别。

【问题讨论】：

标签： python z3 z3py library-path

【解决方案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

【讨论】：