我的情况
我已经安装了 Microsoft Z3 ( Z3 [version 4.3.0 - 64 bit]. (C) 2006 )，它是 pyc Python2 的二进制文件。
我编写了一个Python3包，需要访问z3功能。
为了能够使用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 一起运行吗？
谢谢。 - 如果有任何不清楚的地方，请留下问题评论。
最佳答案
不稳定(正在进行中)支持 Python 3。此功能将在下一个 Z3 版本 (v4.3.2) 中提供。同时，您可以使用 here 中的说明构建 unstable 分支。 .
关于python - 将 Z3Py 与 Python 3.3 结合使用，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/15598669/