1

我想找到一个纯 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？

4

1 回答 1

0

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

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

于 2014-07-04T10:46:59.720 回答