Z3 Pythonバインディング：Z3-pythonを使用する前にinit（Z3_LIBRARY_PATH）を呼び出さなければなりません

Question

Z3 theorem proverをLinuxにインストールし、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という環境変数を設定しようとしたが、それは何の違いが行われていません。

Answer 1

Z3ライブラリをインポートした後、他のZ3のAPIを呼び出す前に

init('/usr/lib64/python2.7/site-packages/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