Привязки Z3 Python: init(Z3_LIBRARY_PATH) должен быть вызван перед использованием Z3-python

Question

Я установил средство проверки теоремы Z3 в Linux и использую его привязки 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

Я попытался установить переменную среды под названием Z3_LIBRARY_PATH до запуска Python, на случай, если это поможет, но это не имеет значения.

Answer 1

После импорта библиотек Z3 позвоните

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

перед вызовом любых других API Z3. Возможно, вам придется скорректировать путь: измените его на путь, где 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