python - 在Python 3.3中使用Z3Py

我的情况

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

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

为了能够在我的Python3软件包中使用pyc二进制文件，我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一起运行？


谢谢。 -如果不清楚，请发表问题评论。

最佳答案

unstable（正在开发中）支持Python3。此功能将在下一个Z3版本（v4.3.2）中提供。同时，您可以使用here中的说明来构建unstable分支。

关于python - 在Python 3.3中使用Z3Py，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/15598669/