Z3 Python bindings: init(Z3_LIBRARY_PATH) must be

问题:

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

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

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

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.

回答1:

After importing the Z3 libraries, call

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

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.)

Example usage:

$ 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