我的情况
我已经安装了 Microsoft Z3 ( Z3 [version 4.3.0 - 64 bit]. (C) 2006)，它是pycPython2 的二进制文件。
我编写了一个需要访问z3功能的 Python3 包。
为了能够将pyc二进制文件与我的 Python3 包一起使用，我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 一起运行？
谢谢。- 如果有任何不清楚的地方，请留下问题评论。