Z3 Python 绑定:在使用 Z3-python 之前必须调用 init(Z3_LIBRARY_PATH) [英] Z3 Python bindings: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python

问题描述

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

I installed the Z3 theorem prover on Linux, and am using its Python bindings (Z3Py). I tried to test a minimal example, but I immediately got the following error:

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

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

How do I fix this and get up and running with Z3?

我不太确定该错误消息的含义.Z3 文档和教程似乎没有对此或 init() 和 Z3-Python 文档 未列出任何名为 init() 的函数.

I'm not quite sure what that error message means. The Z3 documentation and tutorials don't seem to say anything about this or about init(), and the Z3-Python docs don't list any function called init().

更详细地，这是我尝试过的(略有摘录):

In more detail, here is what I tried (lightly excerpted):

$ 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 的环境变量，这可能会有所帮助，但没有任何区别.

I tried setting an environment variable called Z3_LIBRARY_PATH before running Python, on the off chance that would help, but it made no difference.

推荐答案

导入Z3库后，调用

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

在调用任何其他 Z3 API 之前.您可能需要调整路径:将其更改为找到 libz3.so 的路径.(尝试 locate libz3.so 找到它，如果它不在明显的地方.)

before invoking any other Z3 APIs. You might need to adjust the path: change it to the path where libz3.so is found. (Try locate libz3.so to find it, if it's not in an obvious place.)

示例用法:

$ 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

这篇关于Z3 Python 绑定:在使用 Z3-python 之前必须调用 init(Z3_LIBRARY_PATH)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！