私の状況
Microsoft Z3（Z3 [version 4.3.0 - 64 bit]. (C) 2006）をインストールしました。これpycはPython2のバイナリです。
機能にアクセスする必要があるPython3パッケージを作成しましたz3。
pycPython3パッケージでバイナリを使用できるようにするためにdecompyle、z3バイナリを適用し2to3ました。
私の問題
Int('string')Z3Pyは引数<class 'str'>として使用される新しいものを処理できないため、機能しません。'string'
>>> import z3; z3.Int('abc')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File ".\bin\z3.py", line 2931, in Int
return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
File ".\bin\z3.py", line 72, in to_symbol
return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
File ".\bin\z3core.py", line 1430, in Z3_mk_string_symbol
r = lib().Z3_mk_string_symbol(a0, a1)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type
私の質問
decompyle最初にZ3の*.pycファイルを作成する必要があるのは少しハッキーです。では、利用可能なZ3Pyソースコードはありますか？- Python3への既存のZ3Pyポートはすでにありますか？
- Z3PyをPython3で実行する方法について他にアイデアはありますか？
ありがとう。-不明な点がございましたら、質問コメントを残してください。