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

Я установил доказатель теорем 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, на случай, если это поможет, но это не имело значения.


python z3 z3py library-path
person D.W.    schedule 27.03.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

После импорта библиотек 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
person D.W.    schedule 27.03.2017