Verwenden von Z3Py mit Python 3.3
Meine Situation
Ich habe Microsoft Z3 installiert (Z3 [version 4.3.0 - 64 bit]. (C) 2006
) und seinpyc
Binärdateien für Python2.
Ich habe ein Python3-Paket geschrieben, auf das zugegriffen werden mussz3
Funktionalität.
Um das nutzen zu könnenpyc
Binärdateien mit meinem Python3-Paket habe ichdecompyle
dasz3
Binärdateien und angewendet2to3
.
Int('string')
funktioniert nicht, weil Z3Py das Neue nicht verarbeiten kann<class 'str'>
benutzt als'string'
Streit:
>>> 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
Meine FragenEs ist ein bisschen verrückt, das zu müssendecompyle
Z3's*.pyc
Dateien zuerst. Gibt es Z3Py-Quellcodes?Gibt es bereits einen Z3Py-Port für Python3?Irgendeine andere Idee, wie man kommtZ3Py zum Ausführen mit Python3?Vielen Dank. - Wenn etwas unklar ist, hinterlassen Sie bitte eine Frage Kommentar.