在 Python 3.3 中使用 Z3Py

Question

我的情况

我已经安装了 Microsoft Z3 (Z3 [version 4.3.0 - 64 bit]. (C) 2006)，它是 Python2 的 pyc 二进制文件。

我编写了一个 Python3 包，它需要访问 z3 功能。

为了能够将pyc 二进制文件与我的Python3 包一起使用，我decompyle z3 二进制文件并应用了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

我的问题

• 首先需要decompyle Z3 的*.pyc 文件有点麻烦。那么，有没有可用的 Z3Py 源代码？
• 是否已有到 Python3 的 Z3Py 端口？
• 还有其他想法如何让 Z3Py 与 Python3 一起运行？

谢谢。 - 如果有任何不清楚的地方，请留下问题评论。

Answer 1

unstable (work-in-progress) 支持 Python 3。此功能将在下一个 Z3 版本 (v4.3.2) 中提供。同时，您可以使用找到的指令here 构建unstable 分支。