在Python 3.3中使用Z3Py
我的情况
我安装了微软的 Z3（Z3 [版本 4.3.0 - 64 位]（C）2006）以及它的 Python2 版本的 pyc 文件。
我写了一个 Python3 的包，需要用到 z3 的功能。
为了能在我的 Python3 包中使用这些 pyc 文件，我先把 z3 的二进制文件反编译（decompyle），然后用 2to3 工具进行了转换。
我的问题
使用 Int('string') 时出错，因为 Z3Py 不能处理作为 'string' 参数的新 <class 'str'> 类型：
>>> 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
我的问题
- 首先，反编译 Z3 的
*.pyc文件有点麻烦。那么，有没有 Z3Py 的源代码可以用呢？ - 有没有已经存在的 Z3Py 的 Python3 版本？
- 还有其他方法可以让 Z3Py 在 Python3 中运行 吗？
谢谢。如果有什么不清楚的地方，请留言提问。