在谷歌应用引擎上运行 z3

Question

我想找到一个纯 python z3 包，它可以帮助我在谷歌应用引擎中运行 z3。我在本地运行了以下 python 测试并运行：

from z3 import *

    x = Real('x')
    y = Real('y')
    s = Solver()
    s.add(x + y > 5, x > 1, y > 1)
    print s.check()
    print s.model()

但它需要这些文件才能使其工作：z3.pyc、z3consts.pyc、z3core.pyc、z3printer.pyc、z3types.pyc、libz3.dylib。我通过从 z3 codeplex 站点下载构建 z3 来获得这些文件。

因此，将这些文件放在我的 app id 文件夹中的“lib”文件夹中，我尝试了以下 main.py（谷歌提供的“hello world”程序）的改编：

import webapp2
from random import randint
import sys
sys.path.insert(0, 'lib')
from z3 import *

class MainHandler(webapp2.RequestHandler):
    def get(self):
        x = Real('x')
        y = Real('y')
        s = Solver()
        s.add(x + y > 5, x > 1, y > 1)
        self.response.write(s.check())
        self.response.write(s.model())
        self.response.write('Hello world! '+str(randint(7,14)))

app = webapp2.WSGIApplication([('/', MainHandler)], debug=True)

在应用引擎启动器中运行的这段代码为我提供了一个空白页面，并且没有错误消息。

如果我注释掉所有与 z3 相关的代码，我会收到一条 hello world 消息，正如预期的那样。

注意：我已阅读有关如何包含 3rd 方库的文章 14850853，并已使用 BeautifulSoup 成功对其进行了测试。我的问题是关于纯 python z3 库的可用性。

从谷歌关于沙盒的文档中，我很确定 *.pyc 文件没问题，但我认为这些文件需要工作的 (16MB) libz3.dylib 不是纯 python。是否存在 z3 的纯 python 版本，或者是否有其他方法可以在我错过的应用引擎上使用 z3？

Answer 1

Z3 没有纯 Python 版本。 Z3 的所有 API，包括 Python API，都建立在 C API 之上，而 libz3.dll/.so/.dylib 是本机代码。我不确定它是否可以与 Google App Engine 一起使用，但过去我成功地将 libz3.dll 保存在 SQL 数据库中的 blob 中，当我的应用程序启动时，它会从数据库中获取并加载它。

我不确定您打算开发什么应用程序，但请快速查看 Z3 的许可证，以确保在这方面一切正常。